1  /-
  2  Copyright (c) 2019 Mario Carneiro. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Reid Barton, Mario Carneiro, Isabel Longbottom, Scott Morrison
  5  -/
  6  import data.equiv.basic logic.embedding
src         └──────────────┘ └─────────────┘
  7  import data.nat.cast
src         └───────────┘
  8  import data.finset data.fintype
src         └─────────┘ └──────────┘
  9  
 10  /-!
 11  # Combinatorial (pre-)games.
 12  
 13  The basic theory of combinatorial games, following Conway's book `On Numbers and Games`. We
 14  construct "pregames", define an ordering and arithmetic operations on them, then show that the
 15  operations descend to "games", defined via the equivalence relation `p ≈ q ↔ p ≤ q ∧ q ≤ p`.
 16  
 17  The surreal numbers will be built as a quotient of a subtype of pregames.
 18  
 19  A pregame (`pgame` below) is axiomatised via an inductive type, whose sole constructor takes two
 20  types (thought of as indexing the the possible moves for the players Left and Right), and a pair of
 21  functions out of these types to `pgame` (thought of as describing the resulting game after making a
 22  move).
 23  
 24  Combinatorial games themselves, as a quotient of pregames, are constructed in `game.lean`.
 25  
 26  ## Conway induction
 27  
 28  By construction, the induction principle for pregames is exactly "Conway induction". That is, to
 29  prove some predicate `pgame → Prop` holds for all pregames, it suffices to prove that for every
 30  pregame `g`, if the predicate holds for every game resulting from making a move, then it also holds
 31  for `g`.
 32  
 33  While it is often convenient to work "by induction" on pregames, in some situations this becomes
 34  awkward, so we also define accessor functions `left_moves`, `right_moves`, `move_left` and
 35  `move_right`. There is a relation `subsequent p q`, saying that `p` can be reached by playing some
 36  non-empty sequence of moves starting from `q`, an instance `well_founded subsequent`, and a local
 37  tactic `pgame_wf_tac` which is helpful for discharging proof obligations in inductive proofs relying
 38  on this relation.
 39  
 40  ## Order properties
 41  
 42  Pregames have both a `≤` and a `<` relation, which are related in quite a subtle way. In particular,
 43  it is worth noting that in Lean's (perhaps unfortunate?) definition of a `preorder`, we have
 44  `lt_iff_le_not_le : ∀ a b : α, a < b ↔ (a ≤ b ∧ ¬ b ≤ a)`, but this is _not_ satisfied by the usual
 45  `≤` and `<` relations on pregames. (It is satisfied once we restrict to the surreal numbers.) In
 46  particular, `<` is not transitive; there is an example below showing `0 < star ∧ star < 0`.
 47  
 48  We do have
 49  ```
 50  theorem not_le {x y : pgame} : ¬ x ≤ y ↔ y < x := ...
 51  theorem not_lt {x y : pgame} : ¬ x < y ↔ y ≤ x := ...
 52  ```
 53  
 54  The statement `0 ≤ x` means that Left has a good response to any move by Right; in particular, the
 55  theorem `zero_le` below states
 56  ```
 57  0 ≤ x ↔ ∀ j : x.right_moves, ∃ i : (x.move_right j).left_moves, 0 ≤ (x.move_right j).move_left i
 58  ```
 59  On the other hand the statement `0 < x` means that Left has a good move right now; in particular the
 60  theorem `zero_lt` below states
 61  ```
 62  0 < x ↔ ∃ i : left_moves x, ∀ j : right_moves (x.move_left i), 0 < (x.move_left i).move_right j
 63  ```
 64  
 65  The theorems `le_def`, `lt_def`, give a recursive characterisation of each relation, in terms of
 66  themselves two moves later. The theorems `le_def_lt` and `lt_def_lt` give recursive
 67  characterisations of each relation in terms of the other relation one move later.
 68  
 69  We define an equivalence relation `equiv p q ↔ p ≤ q ∧ q ≤ p`. Later, games will be defined as the
 70  quotient by this relation.
 71  
 72  ## Algebraic structures
 73  
 74  We next turn to defining the operations necessary to make games into a commutative additive group.
 75  Addition is defined for $x = \{xL | xR\}$ and $y = \{yL | yR\}$ by $x + y = \{xL + y, x + yL | xR +
 76  y, x + yR\}$. Negation is defined by $\{xL | xR\} = \{-xR | -xL\}$.
 77  
 78  The order structures interact in the expected way with addition, so we have
 79  ```
 80  theorem le_iff_sub_nonneg {x y : pgame} : x ≤ y ↔ 0 ≤ y - x := sorry
 81  theorem lt_iff_sub_pos {x y : pgame} : x < y ↔ 0 < y - x := sorry
 82  ```
 83  
 84  We show that these operations respect the equivalence relation, and hence descend to games. At the
 85  level of games, these operations satisfy all the laws of a commutative group. To prove the necessary
 86  equivalence relations at the level of pregames, we introduce the notion of a `relabelling` of a
 87  game, and show, for example, that there is a relabelling between `x + (y + z)` and `(x + y) + z`.
 88  
 89  ## Future work
 90  * The theory of dominated and reversible positions, and unique normal form for short games.
 91  * Analysis of basic domineering positions.
 92  * Impartial games, nim, and the Sprague-Grundy theorem.
 93  * Hex.
 94  * Temperature.
 95  * The development of surreal numbers, based on this development of combinatorial games, is still
 96    quite incomplete.
 97  
 98  ## References
 99  
100  The material here is all drawn from
101  * [Conway, *On numbers and games*][conway2001]
102  
103  An interested reader may like to formalise some of the material from
104  * [Andreas Blass, *A game semantics for linear logic*][MR1167694]
st                                  
105  * [André Joyal, *Remarques sur la théorie des jeux à deux personnes*][joyal1997]
st                  
106  -/
107  
108  universes u
109  
110  /-- The type of pre-games, before we have quotiented
111    by extensionality. In ZFC, a combinatorial game is constructed from
112    two sets of combinatorial games that have been constructed at an earlier
113    stage. To do this in type theory, we say that a pre-game is built
114    inductively from two families of pre-games indexed over any type
115    in Type u. The resulting type `pgame.{u}` lives in `Type (u+1)`,
116    reflecting that it is a proper class in ZFC. -/
117  inductive pgame : Type (u+1)
118  | mk : ∀ α β : Type u, (α → pgame) → (β → pgame) → pgame
id                  └──┘                  
typ                 └──┘                  
119  
120  namespace pgame
121  
122  /-- Construct a pre-game from list of pre-games describing the available moves for Left and Right. -/
123  -- TODO provide some API describing the interaction with `left_moves`, `right_moves`, `move_left` and `move_right` below.
124  -- TODO define this at the level of games, as well, and perhaps also for finsets of games.
125  def of_lists (L R : list pgame.{0}) : pgame.{0} :=
id                       └──┘ └───┘        └───┘
src                      └──┘ └───┘        └───┘
typ                      └──┘ └───┘        └───┘
doc                           └───┘        └───┘
126  pgame.mk (fin L.length) (fin R.length) (λ i, L.nth_le i.val i.is_lt) (λ j, R.nth_le j.val j.is_lt)
id   └──────┘  └─┘ └─────┘   └─┘ └─────┘       └─────┘ └──┘ └────┘       └─────┘ └──┘ └────┘
src  └──────┘  └─┘  └─────┘   └─┘  └─────┘         └─────┘  └──┘  └────┘         └─────┘  └──┘  └────┘
typ  └──────┘  └─┘ └─────┘   └─┘ └─────┘       └─────┘ └──┘ └────┘       └─────┘ └──┘ └────┘
127  
128  /-- The indexing type for allowable moves by Left. -/
129  def left_moves : pgame → Type u
id                    └───┘ 
src                   └───┘
typ                   └───┘ 
doc                   └───┘
130  | (mk l _ _ _) := l
id      └┘ 
src     └┘
typ     └┘ 
131  /-- The indexing type for allowable moves by Right. -/
132  def right_moves : pgame → Type u
id                     └───┘ 
src                    └───┘
typ                    └───┘ 
doc                    └───┘
133  | (mk _ r _ _) := r
id      └┘   
src     └┘
typ     └┘   
134  
135  /-- The new game after Left makes an allowed move. -/
136  def move_left : Π (g : pgame), left_moves g → pgame
id                         └───┘   └────────┘    └───┘
src                         └───┘   └────────┘     └───┘
typ                        └───┘   └────────┘    └───┘
doc                         └───┘   └────────┘     └───┘
137  | (mk l _ L _) i := L i
id      └┘         
src     └┘
typ     └┘         
138  /-- The new game after Right makes an allowed move. -/
139  def move_right : Π (g : pgame), right_moves g → pgame
id                          └───┘   └─────────┘    └───┘
src                          └───┘   └─────────┘     └───┘
typ                         └───┘   └─────────┘    └───┘
doc                          └───┘   └─────────┘     └───┘
140  | (mk _ r _ R) j := R j
id      └┘         
src     └┘
typ     └┘         
141  
142  @[simp] lemma left_moves_mk {xl xr xL xR} : (⟨xl, xr, xL, xR⟩ : pgame).left_moves = xl := rfl
id                                                 └┘  └┘  └┘  └┘    └───┘ └────────┘   └┘    └─┘
src                                                                  └───┘ └────────┘         └─┘
typ                                                └┘  └┘  └┘  └┘    └───┘ └────────┘   └┘    └─┘
doc    └──┘                                                          └───┘ └────────┘
143  @[simp] lemma move_left_mk {xl xr xL xR i} : (⟨xl, xr, xL, xR⟩ : pgame).move_left i = xL i := rfl
id                                                  └┘  └┘  └┘  └┘    └───┘ └───────┘    └┘     └─┘
src                                                                   └───┘ └───────┘             └─┘
typ                                                 └┘  └┘  └┘  └┘    └───┘ └───────┘    └┘     └─┘
doc    └──┘                                                           └───┘ └───────┘
144  @[simp] lemma right_moves_mk {xl xr xL xR} : (⟨xl, xr, xL, xR⟩ : pgame).right_moves = xr := rfl
id                                                  └┘  └┘  └┘  └┘    └───┘ └─────────┘   └┘    └─┘
src                                                                   └───┘ └─────────┘         └─┘
typ                                                 └┘  └┘  └┘  └┘    └───┘ └─────────┘   └┘    └─┘
doc    └──┘                                                           └───┘ └─────────┘
145  @[simp] lemma move_right_mk {xl xr xL xR j} : (⟨xl, xr, xL, xR⟩ : pgame).move_right j = xR j := rfl
id                                                   └┘  └┘  └┘  └┘    └───┘ └────────┘    └┘     └─┘
src                                                                    └───┘ └────────┘             └─┘
typ                                                  └┘  └┘  └┘  └┘    └───┘ └────────┘    └┘     └─┘
doc    └──┘                                                            └───┘ └────────┘
146  
147  /-- `subsequent p q` says that `p` can be obtained by playing
148    some nonempty sequence of moves from `q`. -/
149  inductive subsequent : pgame → pgame → Prop
id                          └───┘   └───┘
src                         └───┘   └───┘
typ                         └───┘   └───┘
doc                         └───┘   └───┘
150  | left : Π (x : pgame) (i : x.left_moves), subsequent (x.move_left i) x
id                   └───┘       └─────────┘               └────────┘   
src                  └───┘        └─────────┘                └────────┘
typ                  └───┘       └─────────┘               └────────┘   
doc                  └───┘        └─────────┘                └────────┘
151  | right : Π (x : pgame) (j : x.right_moves), subsequent (x.move_right j) x
id                    └───┘       └──────────┘               └─────────┘   
src                   └───┘        └──────────┘                └─────────┘
typ                   └───┘       └──────────┘               └─────────┘   
doc                   └───┘        └──────────┘                └─────────┘
152  | trans : Π (x y z : pgame), subsequent x y → subsequent y z → subsequent x z
id                        └───┘   └────────┘     └────────┘                 
src                       └───┘
typ                       └───┘   └────────┘     └────────┘                 
doc                       └───┘
153  
154  theorem wf_subsequent : well_founded subsequent :=
id                           └──────────┘ └────────┘
src                          └──────────┘ └────────┘
typ                          └──────────┘ └────────┘
doc                                       └────────┘
155  ⟨λ x, begin
id      
typ     
st         └─────
156    induction x with l r L R IHl IHr,
id               
src    └────────┘ └───────────────────┘
typ    └────────┘└───────────────────┘
doc    └────────┘ └───────────────────┘
txt    └────────┘ └───────────────────┘
par    └────────┘ └───────────────────┘
pid              └──────────────────┘
st   ─────────────────────────────────┘└─
157    refine ⟨_, λ y h, _⟩,
src    └─────┘ └─┘ └──────┘
typ    └─────┘ └─┘ └──────┘
doc    └─────┘ └─┘ └──────┘
txt    └─────┘ └─┘ └──────┘
par    └─────┘ └─┘ └──────┘
pid           └─┘ └──────┘
st   ─────────────────────┘└─
158    generalize_hyp e : mk l r L R = x at h,
id                        └┘    
src    └─────────────────┘└┘      └───┘
typ    └─────────────────┘└┘  └───┘
doc    └─────────────────┘        └───┘
txt    └─────────────────┘        └───┘
par    └─────────────────┘        └───┘
pid                  └┘└┘        └───┘
st   ───────────────────────────────────────┘└─
159    induction h with _ i _ j a b _ h1 h2 IH1 IH2; subst e,
id                                                        
src    └────────┘ └───────────────────────────────┘  └────┘
typ    └────────┘└───────────────────────────────┘  └────┘
doc    └────────┘ └───────────────────────────────┘  └────┘
txt    └────────┘ └───────────────────────────────┘  └────┘
par    └────────┘ └───────────────────────────────┘  └────┘
pid              └──────────────────────────────┘       
st   ──────────────────────────────────────────────────────┘└─
160    { apply IHl },
src      └────┘   
typ      └────┘   
doc      └────┘   
txt      └────┘   
par      └────┘   
pid              
st   ───┘└────────┘└┘
161    { apply IHr },
src      └────┘   
typ      └────┘   
doc      └────┘   
txt      └────┘   
par      └────┘   
pid              
st   ───┘└────────┘└┘
162    { exact acc.inv (IH2 rfl) h1 }
id             └─────┘  └─┘ └─┘  └┘
src      └────┘└─────┘    └─┘└┘  
typ      └────┘└─────┘ └─┘└─┘└┘└┘
doc      └────┘              └┘  
txt      └────┘              └┘  
par      └────┘              └┘  
pid                         └┘  
st   ──────────────────────────────┘└─
163  end⟩
st   ──┘
164  
165  instance : has_well_founded pgame :=
id              └──────────────┘ └───┘
src             └──────────────┘ └───┘
typ             └──────────────┘ └───┘
doc                              └───┘
166  { r := subsequent,
id          └────────┘
src         └────────┘
typ         └────────┘
doc         └────────┘
167    wf := wf_subsequent }
id           └───────────┘
src          └───────────┘
typ          └───────────┘
168  
169  /-- A move by Left produces a subsequent game. (For use in pgame_wf_tac.) -/
170  lemma subsequent.left_move {xl xr} {xL : xl → pgame} {xR : xr → pgame} {i : xl} :
id                                            └┘   └───┘        └┘   └───┘       └┘
src                                                └───┘             └───┘
typ                                           └┘   └───┘        └┘   └───┘       └┘
doc                                                └───┘             └───┘
171    subsequent (xL i) (mk xl xr xL xR) :=
id     └────────┘  └┘    └┘ └┘ └┘ └┘ └┘
src    └────────┘         └┘
typ    └────────┘  └┘    └┘ └┘ └┘ └┘ └┘
doc    └────────┘
172  subsequent.left (mk xl xr xL xR) i
id   └─────────────┘  └┘ └┘ └┘ └┘ └┘  
src  └─────────────┘  └┘
typ  └─────────────┘  └┘ └┘ └┘ └┘ └┘  
173  /-- A move by Right produces a subsequent game. (For use in pgame_wf_tac.) -/
174  lemma subsequent.right_move {xl xr} {xL : xl → pgame} {xR : xr → pgame} {j : xr} :
id                                             └┘   └───┘        └┘   └───┘       └┘
src                                                 └───┘             └───┘
typ                                            └┘   └───┘        └┘   └───┘       └┘
doc                                                 └───┘             └───┘
175    subsequent (xR j) (mk xl xr xL xR) :=
id     └────────┘  └┘    └┘ └┘ └┘ └┘ └┘
src    └────────┘         └┘
typ    └────────┘  └┘    └┘ └┘ └┘ └┘ └┘
doc    └────────┘
176  subsequent.right (mk xl xr xL xR) j
id   └──────────────┘  └┘ └┘ └┘ └┘ └┘  
src  └──────────────┘  └┘
typ  └──────────────┘  └┘ └┘ └┘ └┘ └┘  
177  
178  /-- A local tactic for proving well-foundedness of recursive definitions involving pregames. -/
179  meta def pgame_wf_tac :=
id            └──────────┘
typ           └──────────┘
180  `[solve_by_elim
src    └─────────────
typ    └─────────────
doc    └─────────────
txt    └─────────────
par    └─────────────
pid                 
181    [psigma.lex.left, psigma.lex.right,
src  ──┘               └┘                └─
typ  ──┘               └┘                └─
doc  ──┘               └┘                └─
txt  ──┘               └┘                └─
par  ──┘               └┘                └─
pid  ─┘               └┘                └─
182     subsequent.left_move, subsequent.right_move,
src  ──┘                    └┘                     └─
typ  ──┘                    └┘                     └─
doc  ──┘                    └┘                     └─
txt  ──┘                    └┘                     └─
par  ──┘                    └┘                     └─
pid  ──┘                    └┘                     └─
183     subsequent.left, subsequent.right, subsequent.trans]
src  ──┘               └┘                └┘                └─
typ  ──┘               └┘                └┘                └─
doc  ──┘               └┘                └┘                └─
txt  ──┘               └┘                └┘                └─
par  ──┘               └┘                └┘                └─
pid  ──┘               └┘                └┘                
184    { max_rep := 6 }]
src  ─┘ └─────────────┘
typ  ─┘ └─────────────┘
doc  ─┘ └─────────────┘
txt  ─┘ └─────────────┘
par  ─┘ └─────────────┘
pid  ─┘ └─────────────┘
185  
186  /-- The pre-game `zero` is defined by `0 = { | }`. -/
187  instance : has_zero pgame := ⟨⟨pempty, pempty, pempty.elim, pempty.elim⟩⟩
id              └──────┘ └───┘      └────┘  └────┘  └─────────┘  └─────────┘
src             └──────┘ └───┘      └────┘  └────┘  └─────────┘  └─────────┘
typ             └──────┘ └───┘      └────┘  └────┘  └─────────┘  └─────────┘
doc                      └───┘      └────┘  └────┘
188  
189  @[simp] lemma zero_left_moves : (0 : pgame).left_moves = pempty := rfl
id                                        └───┘ └────────┘   └────┘    └─┘
src                                       └───┘ └────────┘   └────┘    └─┘
typ                                       └───┘ └────────┘   └────┘    └─┘
doc    └──┘                               └───┘ └────────┘    └────┘
190  @[simp] lemma zero_right_moves : (0 : pgame).right_moves = pempty := rfl
id                                         └───┘ └─────────┘   └────┘    └─┘
src                                        └───┘ └─────────┘   └────┘    └─┘
typ                                        └───┘ └─────────┘   └────┘    └─┘
doc    └──┘                                └───┘ └─────────┘    └────┘
191  
192  instance : inhabited pgame := ⟨0⟩
id              └───────┘ └───┘
src             └───────┘ └───┘
typ             └───────┘ └───┘
doc                       └───┘
193  
194  /-- The pre-game `one` is defined by `1 = { 0 | }`. -/
195  instance : has_one pgame := ⟨⟨punit, pempty, λ _, 0, pempty.elim⟩⟩
id              └─────┘ └───┘      └───┘  └────┘         └─────────┘
src             └─────┘ └───┘      └───┘  └────┘          └─────────┘
typ             └─────┘ └───┘      └───┘  └────┘         └─────────┘
doc                     └───┘             └────┘
196  
197  @[simp] lemma one_left_moves : (1 : pgame).left_moves = punit := rfl
id                                       └───┘ └────────┘   └───┘    └─┘
src                                      └───┘ └────────┘   └───┘    └─┘
typ                                      └───┘ └────────┘   └───┘    └─┘
doc    └──┘                              └───┘ └────────┘
198  @[simp] lemma one_move_left : (1 : pgame).move_left punit.star = 0 := rfl
id                                      └───┘ └───────┘  └────────┘       └─┘
src                                     └───┘ └───────┘  └────────┘       └─┘
typ                                     └───┘ └───────┘  └────────┘       └─┘
doc    └──┘                             └───┘ └───────┘
199  @[simp] lemma one_right_moves : (1 : pgame).right_moves = pempty := rfl
id                                        └───┘ └─────────┘   └────┘    └─┘
src                                       └───┘ └─────────┘   └────┘    └─┘
typ                                       └───┘ └─────────┘   └────┘    └─┘
doc    └──┘                               └───┘ └─────────┘    └────┘
200  
201  /-- Define simultaneously by mutual induction the `<=` and `<`
202    relation on pre-games. The ZFC definition says that `x = {xL | xR}`
203    is less or equal to `y = {yL | yR}` if `∀ x₁ ∈ xL, x₁ < y`
204    and `∀ y₂ ∈ yR, x < y₂`, where `x < y` is the same as `¬ y <= x`.
205    This is a tricky induction because it only decreases one side at
206    a time, and it also swaps the arguments in the definition of `<`.
207    The solution is to define `x < y` and `x <= y` simultaneously. -/
208  def le_lt : Π (x y : pgame), Prop × Prop
id                       └───┘        
src                       └───┘        
typ                      └───┘        
doc                       └───┘
209  | (mk xl xr xL xR) (mk yl yr yL yR) :=
id         └┘ └┘ └┘ └┘   └┘ └┘ └┘ └┘ └┘
src                      └┘
typ        └┘ └┘ └┘ └┘   └┘ └┘ └┘ └┘ └┘
210    -- the orderings of the clauses here are carefully chosen so that
211    --   and.left/or.inl refer to moves by Left, and
212    --   and.right/or.inr refer to moves by Right.
213  ((∀ i : xl, (le_lt (xL i) ⟨yl, yr, yL, yR⟩).2) ∧ (∀ j : yr, (le_lt ⟨xl, xr, xL, xR⟩ (yR j)).2),
id               └───┘                                        └───┘                        
src                                                                                          
typ              └───┘                                        └───┘                        
214    (∃ i : yl, (le_lt ⟨xl, xr, xL, xR⟩ (yL i)).1) ∨ (∃ j : xr, (le_lt (xR j) ⟨yl, yr, yL, yR⟩).1))
id               └───┘                                      └───┘                        
src                                                                                        
typ              └───┘                                      └───┘                        
215  using_well_founded { dec_tac := pgame_wf_tac }
id                                   └──────────┘
src                                  └──────────┘
typ                                  └──────────┘
doc                                  └──────────┘
216  
217  instance : has_le pgame := ⟨λ x y, (le_lt x y).1⟩
id              └────┘ └───┘           └───┘   
src             └────┘ └───┘             └───┘     
typ             └────┘ └───┘           └───┘   
doc                    └───┘             └───┘
218  instance : has_lt pgame := ⟨λ x y, (le_lt x y).2⟩
id              └────┘ └───┘           └───┘   
src             └────┘ └───┘             └───┘     
typ             └────┘ └───┘           └───┘   
doc                    └───┘             └───┘
219  
220  /-- Definition of `x ≤ y` on pre-games built using the constructor. -/
221  @[simp] theorem mk_le_mk {xl xr xL xR yl yr yL yR} :
doc    └──┘
222    (⟨xl, xr, xL, xR⟩ : pgame) ≤ ⟨yl, yr, yL, yR⟩ ↔
id       └┘  └┘  └┘  └┘    └───┘    └┘  └┘  └┘  └┘  
src                        └───┘                    
typ      └┘  └┘  └┘  └┘    └───┘    └┘  └┘  └┘  └┘  
doc                        └───┘
223    (∀ i, xL i < ⟨yl, yr, yL, yR⟩) ∧
id          └┘    └┘  └┘  └┘  └┘   
src                                  
typ         └┘    └┘  └┘  └┘  └┘   
224    (∀ j, (⟨xl, xr, xL, xR⟩ : pgame) < yR j) := iff.rfl
id            └┘  └┘  └┘  └┘    └───┘   └┘      └─────┘
src                              └───┘            └─────┘
typ           └┘  └┘  └┘  └┘    └───┘   └┘      └─────┘
doc                              └───┘
225  
226  /-- Definition of `x ≤ y` on pre-games, in terms of `<` -/
227  theorem le_def_lt {x y : pgame} : x ≤ y ↔
id                            └───┘       
src                           └───┘         
typ                           └───┘       
doc                           └───┘
228    (∀ i : x.left_moves, x.move_left i < y) ∧
id            └─────────┘  └────────┘     
src            └─────────┘   └────────┘       
typ           └─────────┘  └────────┘     
doc            └─────────┘   └────────┘
229    (∀ j : y.right_moves, x < y.move_right j) :=
id            └──────────┘    └─────────┘ 
src            └──────────┘      └─────────┘
typ           └──────────┘    └─────────┘ 
doc            └──────────┘       └─────────┘
230  by { cases x, cases y, refl }
id                      
src       └────┘   └────┘   └───┘
typ       └────┘  └────┘  └───┘
doc       └────┘   └────┘   └───┘
txt       └────┘   └────┘   └───┘
par       └────┘   └────┘   └───┘
pid                           
st     └────────┘└───────┘└─────┘└┘
231  
232  /-- Definition of `x < y` on pre-games built using the constructor. -/
233  @[simp] theorem mk_lt_mk {xl xr xL xR yl yr yL yR} :
doc    └──┘
234    (⟨xl, xr, xL, xR⟩ : pgame) < ⟨yl, yr, yL, yR⟩ ↔
id       └┘  └┘  └┘  └┘    └───┘    └┘  └┘  └┘  └┘  
src                        └───┘                    
typ      └┘  └┘  └┘  └┘    └───┘    └┘  └┘  └┘  └┘  
doc                        └───┘
235    (∃ i, (⟨xl, xr, xL, xR⟩ : pgame) ≤ yL i) ∨
id          └┘  └┘  └┘  └┘    └───┘   └┘   
src                            └───┘         
typ         └┘  └┘  └┘  └┘    └───┘   └┘   
doc                              └───┘
236    (∃ j, xR j ≤ ⟨yl, yr, yL, yR⟩) := iff.rfl
id        └┘    └┘  └┘  └┘  └┘      └─────┘
src                                   └─────┘
typ       └┘    └┘  └┘  └┘  └┘      └─────┘
237  
238  /-- Definition of `x < y` on pre-games, in terms of `≤` -/
239  theorem lt_def_le {x y : pgame} : x < y ↔
id                            └───┘       
src                           └───┘         
typ                           └───┘       
doc                           └───┘
240    (∃ i : y.left_moves, x ≤ y.move_left i) ∨
id           └─────────┘   └────────┘   
src           └─────────┘     └────────┘    
typ          └─────────┘   └────────┘   
doc            └─────────┘       └────────┘
241    (∃ j : x.right_moves, x.move_right j ≤ y) :=
id           └──────────┘ └─────────┘   
src           └──────────┘  └─────────┘   
typ          └──────────┘ └─────────┘   
doc            └──────────┘   └─────────┘
242  by { cases x, cases y, refl }
id                      
src       └────┘   └────┘   └───┘
typ       └────┘  └────┘  └───┘
doc       └────┘   └────┘   └───┘
txt       └────┘   └────┘   └───┘
par       └────┘   └────┘   └───┘
pid                           
st     └────────┘└───────┘└─────┘└┘
243  
244  /-- The definition of `x ≤ y` on pre-games, in terms of `≤` two moves later. -/
245  theorem le_def {x y : pgame} : x ≤ y ↔
id                         └───┘       
src                        └───┘         
typ                        └───┘       
doc                        └───┘
246    (∀ i : x.left_moves,
id            └─────────┘
src            └─────────┘
typ           └─────────┘
doc            └─────────┘
247     (∃ i' : y.left_moves, x.move_left i ≤ y.move_left i') ∨
id             └─────────┘ └────────┘   └────────┘ └┘  
src             └─────────┘  └────────┘     └────────┘     
typ            └─────────┘ └────────┘   └────────┘ └┘  
doc              └─────────┘   └────────┘      └────────┘
248     (∃ j : (x.move_left i).right_moves, (x.move_left i).move_right j ≤ y)) ∧
id             └────────┘  └─────────┘   └────────┘  └────────┘       
src             └────────┘   └─────────┘    └────────┘   └────────┘         
typ            └────────┘  └─────────┘   └────────┘  └────────┘       
doc              └────────┘   └─────────┘     └────────┘   └────────┘
249    (∀ j : y.right_moves,
id            └──────────┘
src            └──────────┘
typ           └──────────┘
doc            └──────────┘
250     (∃ i : (y.move_right j).left_moves, x ≤ (y.move_right j).move_left i) ∨
id             └─────────┘  └────────┘     └─────────┘  └───────┘    
src             └─────────┘   └────────┘       └─────────┘   └───────┘     
typ            └─────────┘  └────────┘     └─────────┘  └───────┘    
doc              └─────────┘   └────────┘         └─────────┘   └───────┘
251     (∃ j' : x.right_moves, x.move_right j' ≤ y.move_right j)) :=
id             └──────────┘ └─────────┘ └┘  └─────────┘ 
src             └──────────┘  └─────────┘      └─────────┘
typ            └──────────┘ └─────────┘ └┘  └─────────┘ 
doc              └──────────┘   └─────────┘       └─────────┘
252  begin
st   └─────
253    rw [le_def_lt],
id         └───────┘
src    └──┘└───────┘
typ    └──┘└───────┘
doc    └──┘└───────┘
txt    └──┘         
par    └──┘         
pid      └┘         
st   ──────────────┘└──
254    conv { to_lhs, simp only [lt_def_le] },
id                               └───────┘
src    └─────┘└────┘└┘└─────────┘└───────┘└┘
typ    └─────┘└────┘└┘└─────────┘└───────┘└┘
doc                              └───────┘
txt    └─────┘└────┘└┘└─────────┘         └┘
par    └─────┘└────┘└┘└─────────┘         └┘
pid        └───────────────────┘         └─┘
st   ───────┘└─────┘└──────────────────────┘└┘
255  end
st   ──┘
256  
257  /-- The definition of `x < y` on pre-games, in terms of `<` two moves later. -/
258  theorem lt_def {x y : pgame} : x < y ↔
id                         └───┘       
src                        └───┘         
typ                        └───┘       
doc                        └───┘
259    (∃ i : y.left_moves,
id           └─────────┘
src           └─────────┘
typ          └─────────┘
doc            └─────────┘
260      (∀ i' : x.left_moves, x.move_left i' < y.move_left i) ∧
id               └─────────┘  └────────┘ └┘  └────────┘   
src               └─────────┘   └────────┘      └────────┘    
typ              └─────────┘  └────────┘ └┘  └────────┘   
doc               └─────────┘   └────────┘       └────────┘
261      (∀ j : (y.move_left i).right_moves, x < (y.move_left i).move_right j)) ∨
id               └────────┘  └─────────┘      └────────┘  └────────┘     
src               └────────┘   └─────────┘        └────────┘   └────────┘      
typ              └────────┘  └─────────┘      └────────┘  └────────┘     
doc               └────────┘   └─────────┘         └────────┘   └────────┘
262    (∃ j : x.right_moves,
id           └──────────┘
src           └──────────┘
typ          └──────────┘
doc            └──────────┘
263      (∀ i : (x.move_right j).left_moves, (x.move_right j).move_left i < y) ∧
id               └─────────┘  └────────┘    └─────────┘  └───────┘      
src               └─────────┘   └────────┘     └─────────┘   └───────┘        
typ              └─────────┘  └────────┘    └─────────┘  └───────┘      
doc               └─────────┘   └────────┘     └─────────┘   └───────┘
264      (∀ j' : y.right_moves, x.move_right j < y.move_right j')) :=
id               └──────────┘  └─────────┘   └─────────┘ └┘
src               └──────────┘   └─────────┘     └─────────┘
typ              └──────────┘  └─────────┘   └─────────┘ └┘
doc               └──────────┘   └─────────┘      └─────────┘
265  begin
st   └─────
266    rw [lt_def_le],
id         └───────┘
src    └──┘└───────┘
typ    └──┘└───────┘
doc    └──┘└───────┘
txt    └──┘         
par    └──┘         
pid      └┘         
st   ──────────────┘└──
267    conv { to_lhs, simp only [le_def_lt] },
id                               └───────┘
src    └─────┘└────┘└┘└─────────┘└───────┘└┘
typ    └─────┘└────┘└┘└─────────┘└───────┘└┘
doc                              └───────┘
txt    └─────┘└────┘└┘└─────────┘         └┘
par    └─────┘└────┘└┘└─────────┘         └┘
pid        └───────────────────┘         └─┘
st   ───────┘└─────┘└──────────────────────┘└┘
268  end
st   ──┘
269  
270  /-- The definition of `x ≤ 0` on pre-games, in terms of `≤ 0` two moves later. -/
271  theorem le_zero {x : pgame} : x ≤ 0 ↔
id                        └───┘        
src                       └───┘         
typ                       └───┘        
doc                       └───┘
272    ∀ i : x.left_moves, ∃ j : (x.move_left i).right_moves, (x.move_left i).move_right j ≤ 0 :=
id           └─────────┘        └────────┘  └─────────┘   └────────┘  └────────┘   
src           └─────────┘         └────────┘   └─────────┘    └────────┘   └────────┘    
typ          └─────────┘        └────────┘  └─────────┘   └────────┘  └────────┘   
doc           └─────────┘          └────────┘   └─────────┘     └────────┘   └────────┘
273  begin
st   └─────
274    rw le_def,
id        └────┘
src    └─┘└────┘
typ    └─┘└────┘
doc    └─┘└────┘
txt    └─┘
par    └─┘
pid      
st   ──────────┘└─
275    dsimp,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
276    simp [forall_pempty, exists_pempty]
id           └───────────┘  └───────────┘
src    └────┘└───────────┘└┘└───────────┘└┘
typ    └────┘└───────────┘└┘└───────────┘└┘
doc    └────┘             └┘             └┘
txt    └────┘             └┘             └┘
par    └────┘             └┘             └┘
pid                     └┘             
st   ─────────────────────────────────────┘
277  end
st   └─┘
278  
279  /-- The definition of `0 ≤ x` on pre-games, in terms of `0 ≤` two moves later. -/
280  theorem zero_le {x : pgame} : 0 ≤ x ↔
id                        └───┘        
src                       └───┘         
typ                       └───┘        
doc                       └───┘
281    ∀ j : x.right_moves, ∃ i : (x.move_right j).left_moves, 0 ≤ (x.move_right j).move_left i :=
id           └──────────┘        └─────────┘  └────────┘      └─────────┘  └───────┘  
src           └──────────┘         └─────────┘   └────────┘       └─────────┘   └───────┘
typ          └──────────┘        └─────────┘  └────────┘      └─────────┘  └───────┘  
doc           └──────────┘          └─────────┘   └────────┘         └─────────┘   └───────┘
282  begin
st   └─────
283    rw le_def,
id        └────┘
src    └─┘└────┘
typ    └─┘└────┘
doc    └─┘└────┘
txt    └─┘
par    └─┘
pid      
st   ──────────┘└─
284    dsimp,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
285    simp [forall_pempty, exists_pempty]
id           └───────────┘  └───────────┘
src    └────┘└───────────┘└┘└───────────┘└┘
typ    └────┘└───────────┘└┘└───────────┘└┘
doc    └────┘             └┘             └┘
txt    └────┘             └┘             └┘
par    └────┘             └┘             └┘
pid                     └┘             
st   ─────────────────────────────────────┘
286  end
st   └─┘
287  
288  /-- The definition of `x < 0` on pre-games, in terms of `< 0` two moves later. -/
289  theorem lt_zero {x : pgame} : x < 0 ↔
id                        └───┘        
src                       └───┘         
typ                       └───┘        
doc                       └───┘
290    ∃ j : x.right_moves, ∀ i : (x.move_right j).left_moves, (x.move_right j).move_left i < 0 :=
id          └──────────┘        └─────────┘  └────────┘    └─────────┘  └───────┘   
src          └──────────┘         └─────────┘   └────────┘     └─────────┘   └───────┘    
typ         └──────────┘        └─────────┘  └────────┘    └─────────┘  └───────┘   
doc           └──────────┘          └─────────┘   └────────┘     └─────────┘   └───────┘
291  begin
st   └─────
292    rw lt_def,
id        └────┘
src    └─┘└────┘
typ    └─┘└────┘
doc    └─┘└────┘
txt    └─┘
par    └─┘
pid      
st   ──────────┘└─
293    dsimp,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
294    simp [forall_pempty, exists_pempty]
id           └───────────┘  └───────────┘
src    └────┘└───────────┘└┘└───────────┘└┘
typ    └────┘└───────────┘└┘└───────────┘└┘
doc    └────┘             └┘             └┘
txt    └────┘             └┘             └┘
par    └────┘             └┘             └┘
pid                     └┘             
st   ─────────────────────────────────────┘
295  end
st   └─┘
296  
297  /-- The definition of `0 < x` on pre-games, in terms of `< x` two moves later. -/
298  theorem zero_lt {x : pgame} : 0 < x ↔
id                        └───┘        
src                       └───┘         
typ                       └───┘        
doc                       └───┘
299    ∃ i : x.left_moves, ∀ j : (x.move_left i).right_moves, 0 < (x.move_left i).move_right j :=
id          └─────────┘        └────────┘  └─────────┘       └────────┘  └────────┘  
src          └─────────┘         └────────┘   └─────────┘        └────────┘   └────────┘
typ         └─────────┘        └────────┘  └─────────┘       └────────┘  └────────┘  
doc           └─────────┘          └────────┘   └─────────┘         └────────┘   └────────┘
300  begin
st   └─────
301    rw lt_def,
id        └────┘
src    └─┘└────┘
typ    └─┘└────┘
doc    └─┘└────┘
txt    └─┘
par    └─┘
pid      
st   ──────────┘└─
302    dsimp,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
303    simp [forall_pempty, exists_pempty]
id           └───────────┘  └───────────┘
src    └────┘└───────────┘└┘└───────────┘└┘
typ    └────┘└───────────┘└┘└───────────┘└┘
doc    └────┘             └┘             └┘
txt    └────┘             └┘             └┘
par    └────┘             └┘             └┘
pid                     └┘             
st   ─────────────────────────────────────┘
304  end
st   └─┘
305  
306  /-- Given a right-player-wins game, provide a response to any move by left. -/
307  noncomputable def right_response {x : pgame} (h : x ≤ 0) (i : x.left_moves) :
id                                         └───┘                 └─────────┘
src                                        └───┘                   └─────────┘
typ                                        └───┘                 └─────────┘
doc                                        └───┘                    └─────────┘
308    (x.move_left i).right_moves :=
id      └────────┘  └─────────┘
src      └────────┘   └─────────┘
typ     └────────┘  └─────────┘
doc      └────────┘   └─────────┘
309  classical.some $ (le_zero.1 h) i
id   └────────────┘    └─────┘    
src  └────────────┘    └─────┘
typ  └────────────┘    └─────┘    
doc                    └─────┘
310  
311  /-- Show that the response for right provided by `right_response`
312      preserves the right-player-wins condition. -/
313  lemma right_response_spec {x : pgame} (h : x ≤ 0) (i : x.left_moves) :
id                                  └───┘                 └─────────┘
src                                 └───┘                   └─────────┘
typ                                 └───┘                 └─────────┘
doc                                 └───┘                    └─────────┘
314    (x.move_left i).move_right (right_response h i) ≤ 0 :=
id      └────────┘  └────────┘   └────────────┘    
src      └────────┘   └────────┘   └────────────┘      
typ     └────────┘  └────────┘   └────────────┘    
doc      └────────┘   └────────┘   └────────────┘
315  classical.some_spec $ (le_zero.1 h) i
id   └─────────────────┘    └─────┘    
src  └─────────────────┘    └─────┘
typ  └─────────────────┘    └─────┘    
doc                         └─────┘
316  
317  /-- Given a left-player-wins game, provide a response to any move by right. -/
318  noncomputable def left_response {x : pgame} (h : 0 ≤ x) (j : x.right_moves) :
id                                        └───┘                 └──────────┘
src                                       └───┘                   └──────────┘
typ                                       └───┘                 └──────────┘
doc                                       └───┘                    └──────────┘
319    (x.move_right j).left_moves :=
id      └─────────┘  └────────┘
src      └─────────┘   └────────┘
typ     └─────────┘  └────────┘
doc      └─────────┘   └────────┘
320  classical.some $ (zero_le.1 h) j
id   └────────────┘    └─────┘    
src  └────────────┘    └─────┘
typ  └────────────┘    └─────┘    
doc                    └─────┘
321  
322  /-- Show that the response for left provided by `left_response`
323      preserves the left-player-wins condition. -/
324  lemma left_response_spec {x : pgame} (h : 0 ≤ x) (j : x.right_moves) :
id                                 └───┘                 └──────────┘
src                                └───┘                   └──────────┘
typ                                └───┘                 └──────────┘
doc                                └───┘                    └──────────┘
325    0 ≤ (x.move_right j).move_left (left_response h j) :=
id         └─────────┘  └───────┘   └───────────┘  
src         └─────────┘   └───────┘   └───────────┘
typ        └─────────┘  └───────┘   └───────────┘  
doc          └─────────┘   └───────┘   └───────────┘
326  classical.some_spec $ (zero_le.1 h) j
id   └─────────────────┘    └─────┘    
src  └─────────────────┘    └─────┘
typ  └─────────────────┘    └─────┘    
doc                         └─────┘
327  
328  theorem lt_of_le_mk {xl xr xL xR y i} :
329    (⟨xl, xr, xL, xR⟩ : pgame) ≤ y → xL i < y :=
id       └┘  └┘  └┘  └┘    └───┘      └┘   
src                        └───┘            
typ      └┘  └┘  └┘  └┘    └───┘      └┘   
doc                        └───┘
330  by cases y; exact λ h, h.1 i
id                             
src     └────┘   └────┘ └──┘ └─┘ 
typ     └────┘  └────┘ └──┘ └─┘
doc     └────┘   └────┘ └──┘ └─┘ 
txt     └────┘   └────┘ └──┘ └─┘ 
par     └────┘   └────┘ └──┘ └─┘ 
pid                   └──┘ └─┘ 
st     └──────────────────────────
331  
src  
typ  
doc  
txt  
par  
pid  
st   
332  theorem lt_of_mk_le {x : pgame} {yl yr yL yR i} :
id                            └───┘
src                           └───┘
typ                           └───┘
doc                           └───┘
333    x ≤ ⟨yl, yr, yL, yR⟩ → x < yR i :=
id        └┘  └┘  └┘  └┘      └┘ 
src                            
typ       └┘  └┘  └┘  └┘      └┘ 
334  by cases x; exact λ h, h.2 i
id                             
src     └────┘   └────┘ └──┘ └─┘ 
typ     └────┘  └────┘ └──┘ └─┘
doc     └────┘   └────┘ └──┘ └─┘ 
txt     └────┘   └────┘ └──┘ └─┘ 
par     └────┘   └────┘ └──┘ └─┘ 
pid                   └──┘ └─┘ 
st     └──────────────────────────
335  
src  
typ  
doc  
txt  
par  
pid  
st   
336  theorem mk_lt_of_le {xl xr xL xR y i} :
337    (by exact xR i ≤ y) → (⟨xl, xr, xL, xR⟩ : pgame) < y :=
id               └┘         └┘  └┘  └┘  └┘    └───┘   
src        └────┘                            └───┘  
typ        └────┘└┘      └┘  └┘  └┘  └┘    └───┘   
doc        └────┘                             └───┘
txt        └────┘    
par        └────┘    
pid                 
st        └─────────────┘
338  by cases y; exact λ h, or.inr ⟨i, h⟩
id                         └────┘  
src     └────┘   └────┘ └──┘└────┘  └┘ └─
typ     └────┘  └────┘ └──┘└────┘ └┘ └─
doc     └────┘   └────┘ └──┘        └┘ └─
txt     └────┘   └────┘ └──┘        └┘ └─
par     └────┘   └────┘ └──┘        └┘ └─
pid                   └──┘        └┘ 
st     └──────────────────────────────────
339  
src  
typ  
doc  
txt  
par  
pid  
st   
340  theorem lt_mk_of_le {x : pgame} {yl yr yL yR i} :
id                            └───┘
src                           └───┘
typ                           └───┘
doc                           └───┘
341    (by exact x ≤ yL i) → x < ⟨yl, yr, yL, yR⟩ :=
id                 └┘        └┘  └┘  └┘  └┘
src        └────┘          
typ        └────┘└┘       └┘  └┘  └┘  └┘
doc        └────┘    
txt        └────┘    
par        └────┘    
pid                 
st        └─────────────┘
342  by cases x; exact λ h, or.inl ⟨i, h⟩
id                         └────┘  
src     └────┘   └────┘ └──┘└────┘  └┘ └─
typ     └────┘  └────┘ └──┘└────┘ └┘ └─
doc     └────┘   └────┘ └──┘        └┘ └─
txt     └────┘   └────┘ └──┘        └┘ └─
par     └────┘   └────┘ └──┘        └┘ └─
pid                   └──┘        └┘ 
st     └──────────────────────────────────
343  
src  
typ  
doc  
txt  
par  
pid  
st   
344  theorem not_le_lt {x y : pgame} :
id                            └───┘
src                           └───┘
typ                           └───┘
doc                           └───┘
345    (¬ x ≤ y ↔ y < x) ∧ (¬ x < y ↔ y ≤ x) :=
id                        
src                             
typ                       
346  begin
st   └─────
347    induction x with xl xr xL xR IHxl IHxr generalizing y,
id               
src    └────────┘ └────────────────────────────────────────┘
typ    └────────┘└────────────────────────────────────────┘
doc    └────────┘ └────────────────────────────────────────┘
txt    └────────┘ └────────────────────────────────────────┘
par    └────────┘ └────────────────────────────────────────┘
pid              └────────────────────────┘└─────────────┘
st   ──────────────────────────────────────────────────────┘└─
348    induction y with yl yr yL yR IHyl IHyr,
id               
src    └────────┘ └─────────────────────────┘
typ    └────────┘└─────────────────────────┘
doc    └────────┘ └─────────────────────────┘
txt    └────────┘ └─────────────────────────┘
par    └────────┘ └─────────────────────────┘
pid              └────────────────────────┘
st   ───────────────────────────────────────┘└─
349    classical,
src    └───────┘
typ    └───────┘
doc    └───────┘
txt    └───────┘
par    └───────┘
st   ──────────┘└─
350    simp only [mk_le_mk, mk_lt_mk,
id                └──────┘  └──────┘
src    └─────────┘└──────┘└┘└──────┘└─
typ    └─────────┘└──────┘└┘└──────┘└─
doc    └─────────┘└──────┘└┘└──────┘└─
txt    └─────────┘        └┘        └─
par    └─────────┘        └┘        └─
pid        └──┘└┘        └┘        └─
st   ─────────────────────────────────
351      not_and_distrib, not_or_distrib, not_forall, not_exists,
id       └─────────────┘  └────────────┘  └────────┘  └────────┘
src  ───┘└─────────────┘└┘└────────────┘└┘└────────┘└┘└────────┘└─
typ  ───┘└─────────────┘└┘└────────────┘└┘└────────┘└┘└────────┘└─
doc  ───┘               └┘              └┘          └┘          └─
txt  ───┘               └┘              └┘          └┘          └─
par  ───┘               └┘              └┘          └┘          └─
pid  ───┘               └┘              └┘          └┘          └─
st   ─────────────────────────────────────────────────────────────
352      and_comm, or_comm, IHxl, IHxr, IHyl, IHyr, iff_self, and_self]
id       └──────┘  └─────┘  └──┘  └──┘  └──┘  └──┘  └──────┘  └──────┘
src  ───┘└──────┘└┘└─────┘└┘    └┘    └┘    └┘    └┘└──────┘└┘└──────┘└┘
typ  ───┘└──────┘└┘└─────┘└┘└──┘└┘└──┘└┘└──┘└┘└──┘└┘└──────┘└┘└──────┘└┘
doc  ───┘        └┘       └┘    └┘    └┘    └┘    └┘        └┘        └┘
txt  ───┘        └┘       └┘    └┘    └┘    └┘    └┘        └┘        └┘
par  ───┘        └┘       └┘    └┘    └┘    └┘    └┘        └┘        └┘
pid  ───┘        └┘       └┘    └┘    └┘    └┘    └┘        └┘        
st   ──────────────────────────────────────────────────────────────────┘
353  end
st   └─┘
354  
355  theorem not_le {x y : pgame} : ¬ x ≤ y ↔ y < x := not_le_lt.1
id                         └───┘               └───────┘
src                        └───┘                   └───────┘
typ                        └───┘               └───────┘
doc                        └───┘
356  theorem not_lt {x y : pgame} : ¬ x < y ↔ y ≤ x := not_le_lt.2
id                         └───┘               └───────┘
src                        └───┘                   └───────┘
typ                        └───┘               └───────┘
doc                        └───┘
357  
358  @[refl] theorem le_refl : ∀ x : pgame, x ≤ x
id                                  └───┘    
src    └──┘                         └───┘    
typ                                 └───┘    
doc    └──┘                          └───┘
359  | ⟨l, r, L, R⟩ :=
360  ⟨λ i, lt_mk_of_le (le_refl _), λ i, mk_lt_of_le (le_refl _)⟩
id        └─────────┘  └─────┘         └─────────┘  └─────┘
src        └─────────┘  └─────┘          └─────────┘  └─────┘
typ       └─────────┘  └─────┘         └─────────┘  └─────┘
361  
362  theorem lt_irrefl (x : pgame) : ¬ x < x :=
id                          └───┘       
src                         └───┘       
typ                         └───┘       
doc                         └───┘
363  not_lt.2 (le_refl _)
id   └────┘   └─────┘
src  └────┘   └─────┘
typ  └────┘   └─────┘
364  
365  theorem ne_of_lt : ∀ {x y : pgame}, x < y → x ≠ y
id                              └───┘          
src                             └───┘            
typ                             └───┘          
doc                              └───┘
366  | x _ h rfl := lt_irrefl x h
id         └─┘    └───────┘
src          └─┘    └───────┘
typ        └─┘    └───────┘
367  
368  theorem le_trans_aux
369    {xl xr} {xL : xl → pgame} {xR : xr → pgame}
id                   └┘   └───┘        └┘   └───┘
src                       └───┘             └───┘
typ                  └┘   └───┘        └┘   └───┘
doc                       └───┘             └───┘
370    {yl yr} {yL : yl → pgame} {yR : yr → pgame}
id                   └┘   └───┘        └┘   └───┘
src                       └───┘             └───┘
typ                  └┘   └───┘        └┘   └───┘
doc                       └───┘             └───┘
371    {zl zr} {zL : zl → pgame} {zR : zr → pgame}
id                   └┘   └───┘        └┘   └───┘
src                       └───┘             └───┘
typ                  └┘   └───┘        └┘   └───┘
doc                       └───┘             └───┘
372    (h₁ : ∀ i, mk yl yr yL yR ≤ mk zl zr zL zR → mk zl zr zL zR ≤ xL i → mk yl yr yL yR ≤ xL i)
id               └┘ └┘ └┘ └┘ └┘  └┘ └┘ └┘ └┘ └┘   └┘ └┘ └┘ └┘ └┘  └┘    └┘ └┘ └┘ └┘ └┘  └┘ 
src               └┘              └┘               └┘                     └┘             
typ              └┘ └┘ └┘ └┘ └┘  └┘ └┘ └┘ └┘ └┘   └┘ └┘ └┘ └┘ └┘  └┘    └┘ └┘ └┘ └┘ └┘  └┘ 
373    (h₂ : ∀ i, zR i ≤ mk xl xr xL xR → mk xl xr xL xR ≤ mk yl yr yL yR → zR i ≤ mk yl yr yL yR) :
id               └┘   └┘ └┘ └┘ └┘ └┘   └┘ └┘ └┘ └┘ └┘  └┘ └┘ └┘ └┘ └┘   └┘   └┘ └┘ └┘ └┘ └┘
src                     └┘               └┘              └┘                     └┘
typ              └┘   └┘ └┘ └┘ └┘ └┘   └┘ └┘ └┘ └┘ └┘  └┘ └┘ └┘ └┘ └┘   └┘   └┘ └┘ └┘ └┘ └┘
374    mk xl xr xL xR ≤ mk yl yr yL yR →
id     └┘ └┘ └┘ └┘ └┘  └┘ └┘ └┘ └┘ └┘
src    └┘              └┘
typ    └┘ └┘ └┘ └┘ └┘  └┘ └┘ └┘ └┘ └┘
375    mk yl yr yL yR ≤ mk zl zr zL zR →
id     └┘ └┘ └┘ └┘ └┘  └┘ └┘ └┘ └┘ └┘
src    └┘              └┘
typ    └┘ └┘ └┘ └┘ └┘  └┘ └┘ └┘ └┘ └┘
376    mk xl xr xL xR ≤ mk zl zr zL zR :=
id     └┘ └┘ └┘ └┘ └┘  └┘ └┘ └┘ └┘ └┘
src    └┘              └┘
typ    └┘ └┘ └┘ └┘ └┘  └┘ └┘ └┘ └┘ └┘
377  λ ⟨xLy, xyR⟩ ⟨yLz, yzR⟩, ⟨
id     └─┘  └─┘  └─┘  └─┘
typ    └─┘  └─┘  └─┘  └─┘
378    λ i, not_le.1 (λ h, not_lt.2 (h₁ _ ⟨yLz, yzR⟩ h) (xLy _)),
id         └────┘       └────┘   └┘              
src         └────┘        └────┘
typ        └────┘       └────┘   └┘              
379    λ i, not_le.1 (λ h, not_lt.2 (h₂ _ h ⟨xLy, xyR⟩) (yzR _))⟩
id         └────┘       └────┘   └┘   
src         └────┘        └────┘
typ        └────┘       └────┘   └┘   
380  
381  @[trans] theorem le_trans {x y z : pgame} : x ≤ y → y ≤ z → x ≤ z :=
id                                      └───┘                
src    └───┘                            └───┘                    
typ                                     └───┘                
doc    └───┘                            └───┘
382  suffices ∀ {x y z : pgame},
id                       └───┘
src                      └───┘
typ                      └───┘
doc                      └───┘
383    (x ≤ y → y ≤ z → x ≤ z) ∧ (y ≤ z → z ≤ x → y ≤ x) ∧ (z ≤ x → x ≤ y → z ≤ y),
id                                                  
src                                                                 
typ                                                 
384  from this.1, begin
id        └──┘
src           
typ       └──┘
st                └─────
385    clear x y z, intros,
src    └─────────┘  └────┘
typ    └─────────┘  └────┘
doc    └─────────┘  └────┘
txt    └─────────┘  └────┘
par    └─────────┘  └────┘
pid         └────┘
st   ────────────┘└──────┘└─
386    induction x with xl xr xL xR IHxl IHxr generalizing y z,
id               
src    └────────┘ └──────────────────────────────────────────┘
typ    └────────┘└──────────────────────────────────────────┘
doc    └────────┘ └──────────────────────────────────────────┘
txt    └────────┘ └──────────────────────────────────────────┘
par    └────────┘ └──────────────────────────────────────────┘
pid              └────────────────────────┘└───────────────┘
st   ────────────────────────────────────────────────────────┘└─
387    induction y with yl yr yL yR IHyl IHyr generalizing z,
id               
src    └────────┘ └────────────────────────────────────────┘
typ    └────────┘└────────────────────────────────────────┘
doc    └────────┘ └────────────────────────────────────────┘
txt    └────────┘ └────────────────────────────────────────┘
par    └────────┘ └────────────────────────────────────────┘
pid              └────────────────────────┘└─────────────┘
st   ──────────────────────────────────────────────────────┘└─
388    induction z with zl zr zL zR IHzl IHzr,
id               
src    └────────┘ └─────────────────────────┘
typ    └────────┘└─────────────────────────┘
doc    └────────┘ └─────────────────────────┘
txt    └────────┘ └─────────────────────────┘
par    └────────┘ └─────────────────────────┘
pid              └────────────────────────┘
st   ───────────────────────────────────────┘└─
389    exact ⟨
src    └────┘ 
typ    └────┘ 
doc    └────┘ 
txt    └────┘ 
par    └────┘ 
pid          
st   ──────────
390      le_trans_aux (λ i, (IHxl _).2.1) (λ i, (IHzr _).2.2),
id                           └──┘                └──┘
src  ───┘              └──┘     └───────┘  └──┘     └─────────
typ  ───┘              └──┘ └──┘└───────┘  └──┘ └──┘└─────────
doc  ───┘              └──┘     └───────┘  └──┘     └─────────
txt  ───┘              └──┘     └───────┘  └──┘     └─────────
par  ───┘              └──┘     └───────┘  └──┘     └─────────
pid  ───┘              └──┘     └───────┘  └──┘     └─────────
st   ──────────────────────────────────────────────────────────
391      le_trans_aux (λ i, (IHyl _).2.2) (λ i, (IHxr _).1),
id                           └──┘                └──┘
src  ───┘              └──┘     └───────┘  └──┘     └───────
typ  ───┘              └──┘ └──┘└───────┘  └──┘ └──┘└───────
doc  ───┘              └──┘     └───────┘  └──┘     └───────
txt  ───┘              └──┘     └───────┘  └──┘     └───────
par  ───┘              └──┘     └───────┘  └──┘     └───────
pid  ───┘              └──┘     └───────┘  └──┘     └───────
st   ────────────────────────────────────────────────────────
392      le_trans_aux (λ i, (IHzl _).1) (λ i, (IHyr _).2.1)⟩,
id       └──────────┘        └──┘              └──┘
src  ───┘└──────────┘  └──┘     └─────┘  └──┘     └───────┘
typ  ───┘└──────────┘  └──┘ └──┘└─────┘  └──┘ └──┘└───────┘
doc  ───┘              └──┘     └─────┘  └──┘     └───────┘
txt  ───┘              └──┘     └─────┘  └──┘     └───────┘
par  ───┘              └──┘     └─────┘  └──┘     └───────┘
pid  ───┘              └──┘     └─────┘  └──┘     └───────┘
st   ──────────────────────────────────────────────────────┘└─
393  end
st   ──┘
394  
395  @[trans] theorem lt_of_le_of_lt {x y z : pgame} (hxy : x ≤ y) (hyz : y < z) : x < z :=
id                                            └───┘                            
src    └───┘                                  └───┘                                
typ                                           └───┘                            
doc    └───┘                                  └───┘
396  begin
st   └─────
397    rw ←not_le at ⊢ hyz,
id         └────┘
src    └──┘└────┘└───────┘
typ    └──┘└────┘└───────┘
doc    └──┘      └───────┘
txt    └──┘      └───────┘
par    └──┘      └───────┘
pid      └┘      └───────┘
st   ────────────────────┘└─
398    exact mt (λ H, le_trans H hxy) hyz
id           └┘       └──────┘   └─┘  └─┘
src    └────┘└┘  └──┘└──────┘    └┘   
typ    └────┘└┘  └──┘└──────┘ └─┘└┘└─┘
doc    └────┘    └──┘            └┘   
txt    └────┘    └──┘            └┘   
par    └────┘    └──┘            └┘   
pid             └──┘            └┘   
st   ────────────────────────────────────┘
399  end
st   └─┘
400  
401  @[trans] theorem lt_of_lt_of_le {x y z : pgame} (hxy : x < y) (hyz : y ≤ z) : x < z :=
id                                            └───┘                            
src    └───┘                                  └───┘                                
typ                                           └───┘                            
doc    └───┘                                  └───┘
402  begin
st   └─────
403    rw ←not_le at ⊢ hxy,
id         └────┘
src    └──┘└────┘└───────┘
typ    └──┘└────┘└───────┘
doc    └──┘      └───────┘
txt    └──┘      └───────┘
par    └──┘      └───────┘
pid      └┘      └───────┘
st   ────────────────────┘└─
404    exact mt (λ H, le_trans hyz H) hxy
id           └┘       └──────┘ └─┘    └─┘
src    └────┘└┘  └──┘└──────┘    └┘   
typ    └────┘└┘  └──┘└──────┘└─┘ └┘└─┘
doc    └────┘    └──┘            └┘   
txt    └────┘    └──┘            └┘   
par    └────┘    └──┘            └┘   
pid             └──┘            └┘   
st   ────────────────────────────────────┘
405  end
st   └─┘
406  
407  /-- Define the equivalence relation on pre-games. Two pre-games
408    `x`, `y` are equivalent if `x ≤ y` and `y ≤ x`. -/
409  def equiv (x y : pgame) : Prop := x ≤ y ∧ y ≤ x
id                    └───┘                  
src                   └───┘                    
typ                   └───┘                  
doc                   └───┘
410  
411  local infix ` ≈ ` := pgame.equiv
id                        └─────────┘
src                       └─────────┘
typ                       └─────────┘
doc                       └─────────┘
412  
413  @[refl] theorem equiv_refl (x) : x ≈ x := ⟨le_refl _, le_refl _⟩
id                                           └─────┘    └─────┘
src    └──┘                                    └─────┘    └─────┘
typ                                          └─────┘    └─────┘
doc    └──┘                             
414  @[symm] theorem equiv_symm {x y} : x ≈ y → y ≈ x | ⟨xy, yx⟩ := ⟨yx, xy⟩
id                                                └┘  └┘
src    └──┘                                      
typ                                               └┘  └┘
doc    └──┘                                      
415  @[trans] theorem equiv_trans {x y z} : x ≈ y → y ≈ z → x ≈ z
id                                                     
src    └───┘                                                
typ                                                    
doc    └───┘                                                
416  | ⟨xy, yx⟩ ⟨yz, zy⟩ := ⟨le_trans xy yz, le_trans zy yx⟩
id      └┘  └┘   └┘  └┘      └──────┘        └──────┘
src                          └──────┘        └──────┘
typ     └┘  └┘   └┘  └┘      └──────┘        └──────┘
417  
418  theorem lt_of_lt_of_equiv {x y z} (h₁ : x < y) (h₂ : y ≈ z) : x < z := lt_of_lt_of_le h₁ h₂.1
id                                                                 └────────────┘ └┘ └┘
src                                                                      └────────────┘      
typ                                                                └────────────┘ └┘ └┘
doc                                                         
419  theorem le_of_le_of_equiv {x y z} (h₁ : x ≤ y) (h₂ : y ≈ z) : x ≤ z := le_trans h₁ h₂.1
id                                                                 └──────┘ └┘ └┘
src                                                                      └──────┘      
typ                                                                └──────┘ └┘ └┘
doc                                                         
420  theorem lt_of_equiv_of_lt {x y z} (h₁ : x ≈ y) (h₂ : y < z) : x < z := lt_of_le_of_lt h₁.1 h₂
id                                                                 └────────────┘ └┘  └┘
src                                                                      └────────────┘   
typ                                                                └────────────┘ └┘  └┘
doc                                            
421  theorem le_of_equiv_of_le {x y z} (h₁ : x ≈ y) (h₂ : y ≤ z) : x ≤ z := le_trans h₁.1 h₂
id                                                                 └──────┘ └┘  └┘
src                                                                      └──────┘   
typ                                                                └──────┘ └┘  └┘
doc                                            
422  
423  theorem le_congr {x₁ y₁ x₂ y₂} : x₁ ≈ x₂ → y₁ ≈ y₂ → (x₁ ≤ y₁ ↔ x₂ ≤ y₂)
id                                    └┘  └┘  └┘  └┘    └┘  └┘  └┘  └┘
src                                                                 
typ                                   └┘  └┘  └┘  └┘    └┘  └┘  └┘  └┘
doc                                               
424  | ⟨x12, x21⟩ ⟨y12, y21⟩ := ⟨λ h, le_trans x21 (le_trans h y12), λ h, le_trans x12 (le_trans h y21)⟩
id      └─┘  └─┘   └─┘  └─┘          └──────┘      └──────┘            └──────┘      └──────┘ 
src                                   └──────┘      └──────┘              └──────┘      └──────┘
typ     └─┘  └─┘   └─┘  └─┘          └──────┘      └──────┘            └──────┘      └──────┘ 
425  
426  theorem lt_congr {x₁ y₁ x₂ y₂} (hx : x₁ ≈ x₂) (hy : y₁ ≈ y₂) : x₁ < y₁ ↔ x₂ < y₂ :=
id                                        └┘  └┘        └┘  └┘    └┘  └┘  └┘  └┘
src                                                                          
typ                                       └┘  └┘        └┘  └┘    └┘  └┘  └┘  └┘
doc                                                        
427  not_le.symm.trans $ (not_congr (le_congr hy hx)).trans not_le
id   └────┘└───┘└────┘    └───────┘  └──────┘ └┘ └┘  └───┘  └────┘
src  └────┘└───┘└────┘    └───────┘  └──────┘        └───┘  └────┘
typ  └────┘└───┘└────┘    └───────┘  └──────┘ └┘ └┘  └───┘  └────┘
428  
429  /-- `restricted x y` says that Left always has no more moves in `x` than in `y`,
430       and Right always has no more moves in `y` than in `x` -/
431  inductive restricted : pgame.{u} → pgame.{u} → Type (u+1)
id                          └───┘       └───┘
src                         └───┘       └───┘
typ                         └───┘       └───┘
doc                         └───┘       └───┘
432  | mk : Π {x y : pgame} (L : x.left_moves → y.left_moves) (R : y.right_moves → x.right_moves),
id                   └───┘       └─────────┘  └─────────┘       └──────────┘  └──────────┘
src                  └───┘        └─────────┘    └─────────┘        └──────────┘    └──────────┘
typ                  └───┘       └─────────┘  └─────────┘       └──────────┘  └──────────┘
doc                  └───┘        └─────────┘    └─────────┘        └──────────┘    └──────────┘
433           (∀ (i : x.left_moves), restricted (x.move_left i) (y.move_left (L i))) →
id                   └─────────┘               └────────┘    └────────┘   
src                    └─────────┘                └────────┘      └────────┘
typ                  └─────────┘               └────────┘    └────────┘   
doc                    └─────────┘                └────────┘      └────────┘
434           (∀ (j : y.right_moves), restricted (x.move_right (R j)) (y.move_right j)) → restricted x y
id                   └──────────┘               └─────────┘       └─────────┘                  
src                    └──────────┘                └─────────┘          └─────────┘
typ                  └──────────┘               └─────────┘       └─────────┘                  
doc                    └──────────┘                └─────────┘          └─────────┘
435  
436  /-- The identity restriction. -/
437  @[refl] def restricted.refl : Π (x : pgame), restricted x x
id                                       └───┘   └────────┘  
src    └──┘                               └───┘   └────────┘
typ                                      └───┘   └────────┘  
doc    └──┘                               └───┘   └────────┘
438  | (mk xl xr xL xR) :=
id      └┘
src     └┘
typ     └┘
439    restricted.mk
id     └───────────┘
src    └───────────┘
typ    └───────────┘
440      id id
id       └┘ └┘
src      └┘ └┘
typ      └┘ └┘
441      (λ i, restricted.refl _) (λ j, restricted.refl _)
id            └─────────────┘         └─────────────┘
typ           └─────────────┘         └─────────────┘
442  using_well_founded { dec_tac := pgame_wf_tac }
id                                   └──────────┘
src                                  └──────────┘
typ                                  └──────────┘
doc                                  └──────────┘
443  
444  -- TODO trans for restricted
445  
446  theorem le_of_restricted : Π {x y : pgame} (r : restricted x y), x ≤ y
id                                      └───┘       └────────┘       
src                                      └───┘       └────────┘         
typ                                     └───┘       └────────┘       
doc                                      └───┘       └────────┘
447  | (mk xl xr xL xR) (mk yl yr yL yR)
id                       └┘
src                      └┘
typ                      └┘
448    (restricted.mk L_embedding R_embedding L_restriction R_restriction) :=
id      └───────────┘
src     └───────────┘
typ     └───────────┘
449  begin
st   └─────
450    rw le_def,
id        └────┘
src    └─┘└────┘
typ    └─┘└────┘
doc    └─┘└────┘
txt    └─┘
par    └─┘
pid      
st   ──────────┘└─
451    exact
src    └─────
typ    └─────
doc    └─────
txt    └─────
par    └─────
pid         
st   ────────
452      ⟨λ i, or.inl ⟨L_embedding i, le_of_restricted (L_restriction i)⟩,
id             └────┘  └─────────┘                      └───────────┘
src  ───┘  └──┘└────┘             └┘                               └───
typ  ───┘  └──┘└────┘ └─────────┘ └┘                 └───────────┘ └───
doc  ───┘  └──┘                   └┘                               └───
txt  ───┘  └──┘                   └┘                               └───
par  ───┘  └──┘                   └┘                               └───
pid  ───┘  └──┘                   └┘                               └───
st   ──────────────────────────────────────────────────────────────────────
453       λ i, or.inr ⟨R_embedding i, le_of_restricted (R_restriction i)⟩⟩
id             └────┘  └─────────┘    └──────────────┘  └───────────┘
src  ────┘ └──┘└────┘             └┘                               └──┘
typ  ────┘ └──┘└────┘ └─────────┘ └┘└──────────────┘ └───────────┘ └──┘
doc  ────┘ └──┘                   └┘                               └──┘
txt  ────┘ └──┘                   └┘                               └──┘
par  ────┘ └──┘                   └┘                               └──┘
pid  ────┘ └──┘                   └┘                               └─┘
st   ─────────────────────────────────────────────────────────────────────┘
454  end
st   └─┘
455  
456  /-- `relabelling x y` says that `x` and `y` are really the same game, just dressed up differently.
457    Specifically, there is a bijection between the moves for Left in `x` and in `y`, and similarly
458    for Right, and under these bijections we inductively have `relabelling`s for the consequent games. -/
459  inductive relabelling : pgame.{u} → pgame.{u} → Type (u+1)
id                           └───┘       └───┘
src                          └───┘       └───┘
typ                          └───┘       └───┘
doc                          └───┘       └───┘
460  | mk : Π {x y : pgame} (L : x.left_moves ≃ y.left_moves) (R : x.right_moves ≃ y.right_moves),
id                   └───┘       └─────────┘  └─────────┘       └──────────┘  └──────────┘
src                  └───┘        └─────────┘   └─────────┘        └──────────┘   └──────────┘
typ                  └───┘       └─────────┘  └─────────┘       └──────────┘  └──────────┘
doc                  └───┘        └─────────┘   └─────────┘        └──────────┘   └──────────┘
461           (∀ (i : x.left_moves), relabelling (x.move_left i) (y.move_left (L i))) →
id                   └─────────┘                └────────┘    └────────┘   
src                    └─────────┘                 └────────┘      └────────┘
typ                  └─────────┘                └────────┘    └────────┘   
doc                    └─────────┘                 └────────┘      └────────┘
462           (∀ (j : y.right_moves), relabelling (x.move_right (R.symm j)) (y.move_right j)) →
id                   └──────────┘                └─────────┘  └───┘     └─────────┘ 
src                    └──────────┘                 └─────────┘   └───┘       └─────────┘
typ                  └──────────┘                └─────────┘  └───┘     └─────────┘ 
doc                    └──────────┘                 └─────────┘               └─────────┘
463         relabelling x y
id                       
typ                      
464  
465  /-- If `x` is a relabelling of `y`, then Left and Right have the same moves in either game,
466      so `x` is a restriction of `y`. -/
467  def restricted_of_relabelling : Π {x y : pgame} (r : relabelling x y), restricted x y
id                                           └───┘       └─────────┘     └────────┘  
src                                           └───┘       └─────────┘       └────────┘
typ                                          └───┘       └─────────┘     └────────┘  
doc                                           └───┘       └─────────┘       └────────┘
468  | (mk xl xr xL xR) (mk yl yr yL yR) (relabelling.mk L_equiv R_equiv L_relabelling R_relabelling) :=
id                       └┘               └────────────┘ └─────┘ └─────┘ └───────────┘ └───────────┘
src                      └┘               └────────────┘
typ                      └┘               └────────────┘ └─────┘ └─────┘ └───────────┘ └───────────┘
469  restricted.mk L_equiv.to_embedding R_equiv.symm.to_embedding
id   └───────────┘        └───────────┘        └───┘└───────────┘
src  └───────────┘        └───────────┘        └───┘└───────────┘
typ  └───────────┘        └───────────┘        └───┘└───────────┘
470    (λ i, restricted_of_relabelling (L_relabelling i))
id          └───────────────────────┘                
typ         └───────────────────────┘                
471    (λ j, restricted_of_relabelling (R_relabelling j))
id          └───────────────────────┘                
typ         └───────────────────────┘                
472  
473  -- It's not the case that `restricted x y → restricted y x → relabelling x y`,
474  -- but if we insisted that the maps in a restriction were injective, then one
475  -- could use Schröder-Bernstein for do this.
476  
477  /-- The identity relabelling. -/
478  @[refl] def relabelling.refl : Π (x : pgame), relabelling x x
id                                        └───┘   └─────────┘  
src    └──┘                                └───┘   └─────────┘
typ                                       └───┘   └─────────┘  
doc    └──┘                                └───┘   └─────────┘
479  | (mk xl xr xL xR) :=
id      └┘
src     └┘
typ     └┘
480    relabelling.mk (equiv.refl _) (equiv.refl _)
id     └────────────┘  └────────┘     └────────┘
src    └────────────┘  └────────┘     └────────┘
typ    └────────────┘  └────────┘     └────────┘
481      (λ i, relabelling.refl _) (λ j, relabelling.refl _)
id            └──────────────┘         └──────────────┘
typ           └──────────────┘         └──────────────┘
482  using_well_founded { dec_tac := pgame_wf_tac }
id                                   └──────────┘
src                                  └──────────┘
typ                                  └──────────┘
doc                                  └──────────┘
483  
484  /-- Reverse a relabelling. -/
485  @[symm] def relabelling.symm : Π {x y : pgame}, relabelling x y → relabelling y x
id                                          └───┘   └─────────┘     └─────────┘  
src    └──┘                                  └───┘   └─────────┘       └─────────┘
typ                                         └───┘   └─────────┘     └─────────┘  
doc    └──┘                                  └───┘   └─────────┘       └─────────┘
486  | (mk xl xr xL xR) (mk yl yr yL yR) (relabelling.mk L_equiv R_equiv L_relabelling R_relabelling) :=
id                       └┘               └────────────┘
src                      └┘               └────────────┘
typ                      └┘               └────────────┘
487  begin
st   └─────
488    refine relabelling.mk L_equiv.symm R_equiv.symm _ _,
id            └────────────┘ └──────────┘ └──────────┘
src    └─────┘└────────────┘└──────────┘└──────────┘└──┘
typ    └─────┘└────────────┘└──────────┘└──────────┘└──┘
doc    └─────┘                                      └──┘
txt    └─────┘                                      └──┘
par    └─────┘                                      └──┘
pid                                                └──┘
st   ────────────────────────────────────────────────────┘└─
489    { intro i, simpa using (L_relabelling (L_equiv.symm i)).symm },
id                             └───────────┘  └──────────┘ 
src      └─────┘  └──────────┘               └──────────┘ └──────┘
typ      └─────┘  └──────────┘ └───────────┘ └──────────┘└──────┘
doc      └─────┘  └──────────┘                            └──────┘
txt      └─────┘  └──────────┘                            └──────┘
par      └─────┘  └──────────┘                            └──────┘
pid           └┘       └────┘                            └────┘└┘
st   ───┘└─────┘└──────────────────────────────────────────────────┘└┘
490    { intro j, simpa using (R_relabelling (R_equiv j)).symm }
id                             └───────────┘  └─────┘ 
src      └─────┘  └──────────┘                       └──────┘
typ      └─────┘  └──────────┘ └───────────┘ └─────┘└──────┘
doc      └─────┘  └──────────┘                       └──────┘
txt      └─────┘  └──────────┘                       └──────┘
par      └─────┘  └──────────┘                       └──────┘
pid           └┘       └────┘                       └────┘└┘
st   ──────────┘└─────────────────────────────────────────────┘└─
491  end
st   ──┘
492  
493  -- TODO trans for relabelling?
494  
495  theorem le_of_relabelling {x y : pgame} (r : relabelling x y) : x ≤ y :=
id                                    └───┘       └─────────┘        
src                                   └───┘       └─────────┘          
typ                                   └───┘       └─────────┘        
doc                                   └───┘       └─────────┘
496  le_of_restricted (restricted_of_relabelling r)
id   └──────────────┘  └───────────────────────┘ 
src  └──────────────┘  └───────────────────────┘
typ  └──────────────┘  └───────────────────────┘ 
doc                    └───────────────────────┘
497  
498  /-- A relabelling lets us prove equivalence of games. -/
499  theorem equiv_of_relabelling {x y : pgame} (r : relabelling x y) : x ≈ y :=
id                                       └───┘       └─────────┘        
src                                      └───┘       └─────────┘          
typ                                      └───┘       └─────────┘        
doc                                      └───┘       └─────────┘          
500  ⟨le_of_relabelling r, le_of_relabelling r.symm⟩
id    └───────────────┘   └───────────────┘ └───┘
src   └───────────────┘    └───────────────┘  └───┘
typ   └───────────────┘   └───────────────┘ └───┘
doc                                           └───┘
501  
502  instance {x y : pgame} : has_coe (relabelling x y) (x ≈ y) := ⟨equiv_of_relabelling⟩
id                   └───┘    └─────┘  └─────────┘             └──────────────────┘
src                  └───┘    └─────┘  └─────────┘                 └──────────────────┘
typ                  └───┘    └─────┘  └─────────┘             └──────────────────┘
doc                  └───┘             └─────────┘                 └──────────────────┘
503  
504  /-- Replace the types indexing the next moves for Left and Right by equivalent types. -/
505  def relabel {x : pgame} {xl' xr'} (el : x.left_moves ≃ xl') (er : x.right_moves ≃ xr') :=
id                    └───┘                  └─────────┘  └─┘        └──────────┘  └─┘
src                   └───┘                   └─────────┘              └──────────┘ 
typ                   └───┘                  └─────────┘  └─┘        └──────────┘  └─┘
doc                   └───┘                   └─────────┘              └──────────┘ 
506  pgame.mk xl' xr' (λ i, x.move_left (el.symm i)) (λ j, x.move_right (er.symm j))
id   └──────┘ └─┘ └─┘      └────────┘  └┘└───┘         └─────────┘  └┘└───┘ 
src  └──────┘                └────────┘    └───┘            └─────────┘    └───┘
typ  └──────┘ └─┘ └─┘      └────────┘  └┘└───┘         └─────────┘  └┘└───┘ 
doc                          └────────┘                     └─────────┘
507  
508  @[simp] lemma relabel_move_left {x : pgame} {xl' xr'} (el : x.left_moves ≃ xl') (er : x.right_moves ≃ xr') (i : x.left_moves) :
id                                        └───┘                  └─────────┘  └─┘        └──────────┘  └─┘       └─────────┘
src                                       └───┘                   └─────────┘              └──────────┘             └─────────┘
typ                                       └───┘                  └─────────┘  └─┘        └──────────┘  └─┘       └─────────┘
doc    └──┘                               └───┘                   └─────────┘              └──────────┘             └─────────┘
509    move_left (relabel el er) (el i) = x.move_left i :=
id     └───────┘  └─────┘ └┘ └┘   └┘    └────────┘ 
src    └───────┘  └─────┘                 └────────┘
typ    └───────┘  └─────┘ └┘ └┘   └┘    └────────┘ 
doc    └───────┘  └─────┘                  └────────┘
510  by { dsimp [relabel], simp }
id               └─────┘
src       └─────┘└─────┘  └───┘
typ       └─────┘└─────┘  └───┘
doc       └─────┘└─────┘  └───┘
txt       └─────┘         └───┘
par       └─────┘         └───┘
pid                         
st     └────────────────┘└─────┘└┘
511  @[simp] lemma relabel_move_left' {x : pgame} {xl' xr'} (el : x.left_moves ≃ xl') (er : x.right_moves ≃ xr') (i : xl') :
id                                         └───┘                  └─────────┘  └─┘        └──────────┘  └─┘       └─┘
src                                        └───┘                   └─────────┘              └──────────┘ 
typ                                        └───┘                  └─────────┘  └─┘        └──────────┘  └─┘       └─┘
doc    └──┘                                └───┘                   └─────────┘              └──────────┘ 
512    move_left (relabel el er) i = x.move_left (el.symm i) :=
id     └───────┘  └─────┘ └┘ └┘    └────────┘  └┘└───┘ 
src    └───────┘  └─────┘            └────────┘    └───┘
typ    └───────┘  └─────┘ └┘ └┘    └────────┘  └┘└───┘ 
doc    └───────┘  └─────┘             └────────┘
513  rfl
id   └─┘
src  └─┘
typ  └─┘
514  
515  @[simp] lemma relabel_move_right {x : pgame} {xl' xr'} (el : x.left_moves ≃ xl') (er : x.right_moves ≃ xr') (j : x.right_moves) :
id                                         └───┘                  └─────────┘  └─┘        └──────────┘  └─┘       └──────────┘
src                                        └───┘                   └─────────┘              └──────────┘             └──────────┘
typ                                        └───┘                  └─────────┘  └─┘        └──────────┘  └─┘       └──────────┘
doc    └──┘                                └───┘                   └─────────┘              └──────────┘             └──────────┘
516    move_right (relabel el er) (er j) = x.move_right j :=
id     └────────┘  └─────┘ └┘ └┘   └┘    └─────────┘ 
src    └────────┘  └─────┘                 └─────────┘
typ    └────────┘  └─────┘ └┘ └┘   └┘    └─────────┘ 
doc    └────────┘  └─────┘                  └─────────┘
517  by { dsimp [relabel], simp }
id               └─────┘
src       └─────┘└─────┘  └───┘
typ       └─────┘└─────┘  └───┘
doc       └─────┘└─────┘  └───┘
txt       └─────┘         └───┘
par       └─────┘         └───┘
pid                         
st     └────────────────┘└─────┘└┘
518  @[simp] lemma relabel_move_right' {x : pgame} {xl' xr'} (el : x.left_moves ≃ xl') (er : x.right_moves ≃ xr') (j : xr') :
id                                          └───┘                  └─────────┘  └─┘        └──────────┘  └─┘       └─┘
src                                         └───┘                   └─────────┘              └──────────┘ 
typ                                         └───┘                  └─────────┘  └─┘        └──────────┘  └─┘       └─┘
doc    └──┘                                 └───┘                   └─────────┘              └──────────┘ 
519    move_right (relabel el er) j = x.move_right (er.symm j) :=
id     └────────┘  └─────┘ └┘ └┘    └─────────┘  └┘└───┘ 
src    └────────┘  └─────┘            └─────────┘    └───┘
typ    └────────┘  └─────┘ └┘ └┘    └─────────┘  └┘└───┘ 
doc    └────────┘  └─────┘             └─────────┘
520  rfl
id   └─┘
src  └─┘
typ  └─┘
521  
522  /-- The game obtained by relabelling the next moves is a relabelling of the original game. -/
523  def relabel_relabelling {x : pgame} {xl' xr'} (el : x.left_moves ≃ xl') (er : x.right_moves ≃ xr') :
id                                └───┘                  └─────────┘  └─┘        └──────────┘  └─┘
src                               └───┘                   └─────────┘              └──────────┘ 
typ                               └───┘                  └─────────┘  └─┘        └──────────┘  └─┘
doc                               └───┘                   └─────────┘              └──────────┘ 
524    relabelling x (relabel el er) :=
id     └─────────┘   └─────┘ └┘ └┘
src    └─────────┘    └─────┘
typ    └─────────┘   └─────┘ └┘ └┘
doc    └─────────┘    └─────┘
525  relabelling.mk el er (λ i, by simp) (λ j, by simp)
id   └────────────┘ └┘ └┘                  
src  └────────────┘                └──┘           └──┘
typ  └────────────┘ └┘ └┘         └──┘          └──┘
doc                                └──┘           └──┘
txt                                └──┘           └──┘
par                                └──┘           └──┘
st                                └───┘          └───┘
526  
527  /-- The negation of `{L | R}` is `{-R | -L}`. -/
528  def neg : pgame → pgame
id             └───┘  └───┘
src            └───┘   └───┘
typ            └───┘  └───┘
doc            └───┘   └───┘
529  | ⟨l, r, L, R⟩ := ⟨r, l, λ i, neg (R i), λ i, neg (L i)⟩
id                            └─┘           └─┘    
typ                           └─┘           └─┘    
530  
531  instance : has_neg pgame := ⟨neg⟩
id              └─────┘ └───┘     └─┘
src             └─────┘ └───┘     └─┘
typ             └─────┘ └───┘     └─┘
doc                     └───┘     └─┘
532  
533  @[simp] lemma neg_def {xl xr xL xR} : -(mk xl xr xL xR) = mk xr xl (λ j, -(xR j)) (λ i, -(xL i)) :=
id                                          └┘ └┘ └┘ └┘ └┘   └┘ └┘ └┘       └┘          └┘ 
src                                         └┘               └┘                           
typ                                         └┘ └┘ └┘ └┘ └┘   └┘ └┘ └┘       └┘          └┘ 
doc    └──┘
534  rfl
id   └─┘
src  └─┘
typ  └─┘
535  
536  @[simp] theorem neg_neg : Π {x : pgame}, -(-x) = x
id                                   └───┘       
src                                  └───┘       
typ                                  └───┘       
doc    └──┘                           └───┘
537  | (mk xl xr xL xR) :=
id      └┘
src     └┘
typ     └┘
538  begin
st   └─────
539    dsimp [has_neg.neg, neg],
id                         └─┘
src    └─────┘           └┘└─┘
typ    └─────┘           └┘└─┘
doc    └─────┘           └┘└─┘
txt    └─────┘           └┘   
par    └─────┘           └┘   
pid                    └┘   
st   ─────────────────────────┘└─
540    congr; funext i; apply neg_neg
src    └───┘  └──────┘  └────┘       
typ    └───┘  └──────┘  └────┘       
doc           └──────┘  └────┘       
txt    └───┘  └──────┘  └────┘       
par    └───┘  └──────┘  └────┘       
pid                 └┘              
st   ────────────────────────────────┘
541  end
st   └─┘
542  
543  @[simp] theorem neg_zero : -(0 : pgame) = 0 :=
id                                   └───┘  
src                                  └───┘  
typ                                  └───┘  
doc    └──┘                           └───┘
544  begin
st   └─────
545    dsimp [has_zero.zero, has_neg.neg, neg],
id                                        └─┘
src    └─────┘             └┘           └┘└─┘
typ    └─────┘             └┘           └┘└─┘
doc    └─────┘             └┘           └┘└─┘
txt    └─────┘             └┘           └┘   
par    └─────┘             └┘           └┘   
pid                      └┘           └┘   
st   ────────────────────────────────────────┘└─
546    congr; funext i; cases i
id                            
src    └───┘  └──────┘  └────┘ 
typ    └───┘  └──────┘  └────┘
doc           └──────┘  └────┘ 
txt    └───┘  └──────┘  └────┘ 
par    └───┘  └──────┘  └────┘ 
pid                 └┘        
st   ──────────────────────────┘
547  end
st   └─┘
548  
549  /-- An explicit equivalence between the moves for Left in `-x` and the moves for Right in `x`. -/
550  -- This equivalence is useful to avoid having to use `cases` unnecessarily.
551  def left_moves_neg (x : pgame) : (-x).left_moves ≃ x.right_moves :=
id                           └───┘      └────────┘   └──────────┘
src                          └───┘       └────────┘    └──────────┘
typ                          └───┘      └────────┘   └──────────┘
doc                          └───┘        └────────┘    └──────────┘
552  by { cases x, refl }
id              
src       └────┘   └───┘
typ       └────┘  └───┘
doc       └────┘   └───┘
txt       └────┘   └───┘
par       └────┘   └───┘
pid                   
st     └────────┘└─────┘└┘
553  
554  /-- An explicit equivalence between the moves for Right in `-x` and the moves for Left in `x`. -/
555  def right_moves_neg (x : pgame) : (-x).right_moves ≃ x.left_moves :=
id                            └───┘      └─────────┘   └─────────┘
src                           └───┘       └─────────┘    └─────────┘
typ                           └───┘      └─────────┘   └─────────┘
doc                           └───┘        └─────────┘    └─────────┘
556  by { cases x, refl }
id              
src       └────┘   └───┘
typ       └────┘  └───┘
doc       └────┘   └───┘
txt       └────┘   └───┘
par       └────┘   └───┘
pid                   
st     └────────┘└─────┘└┘
557  
558  @[simp] lemma move_right_left_moves_neg {x : pgame} (i : left_moves (-x)) :
id                                                └───┘       └────────┘  
src                                               └───┘       └────────┘  
typ                                               └───┘       └────────┘  
doc    └──┘                                       └───┘       └────────┘
559    move_right x ((left_moves_neg x) i) = -(move_left (-x) i) :=
id     └────────┘    └────────────┘       └───────┘    
src    └────────┘     └────────────┘         └───────┘  
typ    └────────┘    └────────────┘       └───────┘    
doc    └────────┘     └────────────┘           └───────┘
560  begin
st   └─────
561    induction x,
id               
src    └────────┘
typ    └────────┘
doc    └────────┘
txt    └────────┘
par    └────────┘
pid             
st   ────────────┘└─
562    exact neg_neg.symm
id           └──────────┘
src    └────┘└──────────┘
typ    └────┘└──────────┘
doc    └────┘            
txt    └────┘            
par    └────┘            
pid                     
st   ────────────────────┘
563  end
st   └─┘
564  @[simp] lemma move_left_right_moves_neg_symm {x : pgame} (i : right_moves x) :
id                                                     └───┘       └─────────┘ 
src                                                    └───┘       └─────────┘
typ                                                    └───┘       └─────────┘ 
doc    └──┘                                            └───┘       └─────────┘
565    move_left (-x) ((left_moves_neg x).symm i) = -(move_right x i) :=
id     └───────┘      └────────────┘  └──┘      └────────┘  
src    └───────┘       └────────────┘   └──┘       └────────┘
typ    └───────┘      └────────────┘  └──┘      └────────┘  
doc    └───────┘        └────────────┘                └────────┘
566  by { cases x, refl }
id              
src       └────┘   └───┘
typ       └────┘  └───┘
doc       └────┘   └───┘
txt       └────┘   └───┘
par       └────┘   └───┘
pid                   
st     └────────┘└─────┘└┘
567  @[simp] lemma move_left_right_moves_neg {x : pgame} (i : right_moves (-x)) :
id                                                └───┘       └─────────┘  
src                                               └───┘       └─────────┘  
typ                                               └───┘       └─────────┘  
doc    └──┘                                       └───┘       └─────────┘
568    move_left x ((right_moves_neg x) i) = -(move_right (-x) i) :=
id     └───────┘    └─────────────┘       └────────┘    
src    └───────┘     └─────────────┘         └────────┘  
typ    └───────┘    └─────────────┘       └────────┘    
doc    └───────┘     └─────────────┘           └────────┘
569  begin
st   └─────
570    induction x,
id               
src    └────────┘
typ    └────────┘
doc    └────────┘
txt    └────────┘
par    └────────┘
pid             
st   ────────────┘└─
571    exact neg_neg.symm
id           └──────────┘
src    └────┘└──────────┘
typ    └────┘└──────────┘
doc    └────┘            
txt    └────┘            
par    └────┘            
pid                     
st   ────────────────────┘
572  end
st   └─┘
573  @[simp] lemma move_right_right_moves_neg_symm {x : pgame} (i : left_moves x) :
id                                                      └───┘       └────────┘ 
src                                                     └───┘       └────────┘
typ                                                     └───┘       └────────┘ 
doc    └──┘                                             └───┘       └────────┘
574    move_right (-x) ((right_moves_neg x).symm i) = -(move_left x i) :=
id     └────────┘      └─────────────┘  └──┘      └───────┘  
src    └────────┘       └─────────────┘   └──┘       └───────┘
typ    └────────┘      └─────────────┘  └──┘      └───────┘  
doc    └────────┘        └─────────────┘                └───────┘
575  by { cases x, refl }
id              
src       └────┘   └───┘
typ       └────┘  └───┘
doc       └────┘   └───┘
txt       └────┘   └───┘
par       └────┘   └───┘
pid                   
st     └────────┘└─────┘└┘
576  
577  theorem le_iff_neg_ge : Π {x y : pgame}, x ≤ y ↔ -y ≤ -x
id                                   └───┘         
src                                   └───┘            
typ                                  └───┘         
doc                                   └───┘
578  | (mk xl xr xL xR) (mk yl yr yL yR) :=
id                       └┘
src                      └┘
typ                      └┘
579  begin
st   └─────
580    rw [le_def],
id         └────┘
src    └──┘└────┘
typ    └──┘└────┘
doc    └──┘└────┘
txt    └──┘      
par    └──┘      
pid      └┘      
st   ───────────┘└──
581    rw [le_def],
id         └────┘
src    └──┘└────┘
typ    └──┘└────┘
doc    └──┘└────┘
txt    └──┘      
par    └──┘      
pid      └┘      
st   ───────────┘└──
582    dsimp [neg],
id            └─┘
src    └─────┘└─┘
typ    └─────┘└─┘
doc    └─────┘└─┘
txt    └─────┘   
par    └─────┘   
pid            
st   ────────────┘└─
583    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
584    { intro h,
src      └─────┘
typ      └─────┘
doc      └─────┘
txt      └─────┘
par      └─────┘
pid           └┘
st   ───┘└─────┘└─
585      split,
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
st   ────────┘└─
586      { intro i, have t := h.right i, cases t,
id                            └─────┘         
src        └─────┘  └────────┘└─────┘   └────┘
typ        └─────┘  └────────┘└─────┘  └────┘
doc        └─────┘  └────────┘          └────┘
txt        └─────┘  └────────┘          └────┘
par        └─────┘  └────────┘          └────┘
pid             └┘  └────┘└─┘               
st   ─────┘└─────┘└───────────────────┘└───────┘└─
587        { right, cases t, use (@right_moves_neg (yR i)).symm t_w, convert le_iff_neg_ge.1 t_h, simp },
id                                └─────────────┘  └┘         └─┘          └───────────┘   └─┘
src          └───┘  └────┘   └──┘  └─────────────┘    └──────┘     └──────┘             └─┘     └───┘
typ          └───┘  └────┘  └──┘  └─────────────┘ └┘└──────┘└─┘  └──────┘└───────────┘└─┘└─┘  └───┘
doc          └───┘  └────┘   └──┘  └─────────────┘    └──────┘     └──────┘             └─┘     └───┘
txt          └───┘  └────┘   └──┘                     └──────┘     └──────┘             └─┘     └───┘
par          └───┘  └────┘   └──┘                     └──────┘     └──────┘             └─┘     └───┘
pid                                                 └──────┘                         └─┘         
st   ───────┘└───┘└───────┘└──────────────────────────────────────┘└───────────────────────────┘└─────┘└┘
588        { left, cases t, use t_w, exact le_iff_neg_ge.1 t_h, } },
id                             └─┘        └───────────┘   └─┘
src          └──┘  └────┘   └──┘     └────┘             └─┘
typ          └──┘  └────┘  └──┘└─┘  └────┘└───────────┘└─┘└─┘
doc          └──┘  └────┘   └──┘     └────┘             └─┘
txt          └──┘  └────┘   └──┘     └────┘             └─┘
par          └──┘  └────┘   └──┘     └────┘             └─┘
pid                                                  └─┘
st   ───────────┘└───────┘└───────┘└─────────────────────────┘└────┘
589      { intro j, have t := h.left j, cases t,
id                            └────┘         
src        └─────┘  └────────┘└────┘   └────┘
typ        └─────┘  └────────┘└────┘  └────┘
doc        └─────┘  └────────┘         └────┘
txt        └─────┘  └────────┘         └────┘
par        └─────┘  └────────┘         └────┘
pid             └┘  └────┘└─┘              
st   ────────────┘└──────────────────┘└───────┘└─
590        { right, cases t, use t_w, exact le_iff_neg_ge.1 t_h, },
id                              └─┘        └───────────┘   └─┘
src          └───┘  └────┘   └──┘     └────┘             └─┘
typ          └───┘  └────┘  └──┘└─┘  └────┘└───────────┘└─┘└─┘
doc          └───┘  └────┘   └──┘     └────┘             └─┘
txt          └───┘  └────┘   └──┘     └────┘             └─┘
par          └───┘  └────┘   └──┘     └────┘             └─┘
pid                                                   └─┘
st   ───────┘└───┘└───────┘└───────┘└─────────────────────────┘└──┘
591        { left, cases t, use (@left_moves_neg (xL j)).symm t_w, convert le_iff_neg_ge.1 t_h, simp, } } },
id                               └────────────┘  └┘         └─┘          └───────────┘   └─┘
src          └──┘  └────┘   └──┘  └────────────┘    └──────┘     └──────┘             └─┘     └──┘
typ          └──┘  └────┘  └──┘  └────────────┘ └┘└──────┘└─┘  └──────┘└───────────┘└─┘└─┘  └──┘
doc          └──┘  └────┘   └──┘  └────────────┘    └──────┘     └──────┘             └─┘     └──┘
txt          └──┘  └────┘   └──┘                    └──────┘     └──────┘             └─┘     └──┘
par          └──┘  └────┘   └──┘                    └──────┘     └──────┘             └─┘     └──┘
pid                                               └──────┘                         └─┘
st   ───────────┘└───────┘└─────────────────────────────────────┘└───────────────────────────┘└────┘└──────┘
592    { intro h,
src      └─────┘
typ      └─────┘
doc      └─────┘
txt      └─────┘
par      └─────┘
pid           └┘
st   ──────────┘└─
593      split,
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
st   ────────┘└─
594      { intro i, have t := h.right i, cases t,
id                            └─────┘         
src        └─────┘  └────────┘└─────┘   └────┘
typ        └─────┘  └────────┘└─────┘  └────┘
doc        └─────┘  └────────┘          └────┘
txt        └─────┘  └────────┘          └────┘
par        └─────┘  └────────┘          └────┘
pid             └┘  └────┘└─┘               
st   ─────┘└─────┘└───────────────────┘└───────┘└─
595        { right, cases t, use (@left_moves_neg (xL i)) t_w, convert le_iff_neg_ge.2 _, convert t_h, simp, },
id                                └────────────┘  └┘    └─┘          └───────────┘              └─┘
src          └───┘  └────┘   └──┘  └────────────┘    └─┘     └──────┘             └──┘  └──────┘     └──┘
typ          └───┘  └────┘  └──┘  └────────────┘ └┘└─┘└─┘  └──────┘└───────────┘└──┘  └──────┘└─┘  └──┘
doc          └───┘  └────┘   └──┘  └────────────┘    └─┘     └──────┘             └──┘  └──────┘     └──┘
txt          └───┘  └────┘   └──┘                    └─┘     └──────┘             └──┘  └──────┘     └──┘
par          └───┘  └────┘   └──┘                    └─┘     └──────┘             └──┘  └──────┘     └──┘
pid                                                └─┘                         └──┘         
st   ───────┘└───┘└───────┘└────────────────────────────────┘└─────────────────────────┘└───────────┘└────┘└──┘
596        { left, cases t, use t_w, exact le_iff_neg_ge.2 t_h, } },
id                             └─┘        └───────────┘   └─┘
src          └──┘  └────┘   └──┘     └────┘             └─┘
typ          └──┘  └────┘  └──┘└─┘  └────┘└───────────┘└─┘└─┘
doc          └──┘  └────┘   └──┘     └────┘             └─┘
txt          └──┘  └────┘   └──┘     └────┘             └─┘
par          └──┘  └────┘   └──┘     └────┘             └─┘
pid                                                  └─┘
st   ───────────┘└───────┘└───────┘└─────────────────────────┘└────┘
597      { intro j, have t := h.left j, cases t,
id                            └────┘         
src        └─────┘  └────────┘└────┘   └────┘
typ        └─────┘  └────────┘└────┘  └────┘
doc        └─────┘  └────────┘         └────┘
txt        └─────┘  └────────┘         └────┘
par        └─────┘  └────────┘         └────┘
pid             └┘  └────┘└─┘              
st   ────────────┘└──────────────────┘└───────┘└─
598        { right, cases t, use t_w, exact le_iff_neg_ge.2 t_h, },
id                              └─┘        └───────────┘   └─┘
src          └───┘  └────┘   └──┘     └────┘             └─┘
typ          └───┘  └────┘  └──┘└─┘  └────┘└───────────┘└─┘└─┘
doc          └───┘  └────┘   └──┘     └────┘             └─┘
txt          └───┘  └────┘   └──┘     └────┘             └─┘
par          └───┘  └────┘   └──┘     └────┘             └─┘
pid                                                   └─┘
st   ───────┘└───┘└───────┘└───────┘└─────────────────────────┘└──┘
599        { left, cases t, use (@right_moves_neg (yR j)) t_w, convert le_iff_neg_ge.2 _, convert t_h, simp } } },
id                               └─────────────┘  └┘    └─┘          └───────────┘              └─┘
src          └──┘  └────┘   └──┘  └─────────────┘    └─┘     └──────┘             └──┘  └──────┘     └───┘
typ          └──┘  └────┘  └──┘  └─────────────┘ └┘└─┘└─┘  └──────┘└───────────┘└──┘  └──────┘└─┘  └───┘
doc          └──┘  └────┘   └──┘  └─────────────┘    └─┘     └──────┘             └──┘  └──────┘     └───┘
txt          └──┘  └────┘   └──┘                     └─┘     └──────┘             └──┘  └──────┘     └───┘
par          └──┘  └────┘   └──┘                     └─┘     └──────┘             └──┘  └──────┘     └───┘
pid                                                └─┘                         └──┘                  
st   ───────────┘└───────┘└─────────────────────────────────┘└─────────────────────────┘└───────────┘└─────┘└──────
600  end
st   ──┘
601  using_well_founded { dec_tac := pgame_wf_tac }
id                                   └──────────┘
src                                  └──────────┘
typ                                  └──────────┘
doc                                  └──────────┘
602  
603  theorem neg_congr {x y : pgame} (h : x ≈ y) : -x ≈ -y :=
id                            └───┘               
src                           └───┘                  
typ                           └───┘               
doc                           └───┘                  
604  ⟨le_iff_neg_ge.1 h.2, le_iff_neg_ge.1 h.1⟩
id    └───────────┘     └───────────┘  
src   └───────────┘      └───────────┘   
typ   └───────────┘     └───────────┘  
605  
606  theorem lt_iff_neg_gt : Π {x y : pgame}, x < y ↔ -y < -x :=
id                                    └───┘         
src                                   └───┘            
typ                                   └───┘         
doc                                   └───┘
607  begin
st   └─────
608    classical,
src    └───────┘
typ    └───────┘
doc    └───────┘
txt    └───────┘
par    └───────┘
st   ──────────┘└─
609    intros,
src    └────┘
typ    └────┘
doc    └────┘
txt    └────┘
par    └────┘
st   ───────┘└─
610    rw [←not_le, ←not_le, not_iff_not],
id          └────┘   └────┘  └─────────┘
src    └───┘└────┘└─┘└────┘└┘└─────────┘
typ    └───┘└────┘└─┘└────┘└┘└─────────┘
doc    └───┘      └─┘      └┘           
txt    └───┘      └─┘      └┘           
par    └───┘      └─┘      └┘           
pid      └─┘      └─┘      └┘           
st   ────────────┘└───────┘└───────────┘└──
611    apply le_iff_neg_ge
id           └───────────┘
src    └────┘└───────────┘
typ    └────┘└───────────┘
doc    └────┘             
txt    └────┘             
par    └────┘             
pid                      
st   ─────────────────────┘
612  end
st   └─┘
613  
614  theorem zero_le_iff_neg_le_zero {x : pgame} : 0 ≤ x ↔ -x ≤ 0 :=
id                                        └───┘          
src                                       └───┘            
typ                                       └───┘          
doc                                       └───┘
615  begin
st   └─────
616    convert le_iff_neg_ge,
id             └───────────┘
src    └──────┘└───────────┘
typ    └──────┘└───────────┘
doc    └──────┘
txt    └──────┘
par    └──────┘
pid           
st   ──────────────────────┘└─
617    rw neg_zero
id        └──────┘
src    └─┘└──────┘
typ    └─┘└──────┘
doc    └─┘        
txt    └─┘        
par    └─┘        
pid              
st   ─────────────┘
618  end
st   └─┘
619  
620  theorem le_zero_iff_zero_le_neg {x : pgame} : x ≤ 0 ↔ 0 ≤ -x :=
id                                        └───┘            
src                                       └───┘             
typ                                       └───┘            
doc                                       └───┘
621  begin
st   └─────
622    convert le_iff_neg_ge,
id             └───────────┘
src    └──────┘└───────────┘
typ    └──────┘└───────────┘
doc    └──────┘
txt    └──────┘
par    └──────┘
pid           
st   ──────────────────────┘└─
623    rw neg_zero
id        └──────┘
src    └─┘└──────┘
typ    └─┘└──────┘
doc    └─┘        
txt    └─┘        
par    └─┘        
pid              
st   ─────────────┘
624  end
st   └─┘
625  
626  /-- The sum of `x = {xL | xR}` and `y = {yL | yR}` is `{xL + y, x + yL | xR + y, x + yR}`. -/
627  def add (x y : pgame) : pgame :=
id                  └───┘    └───┘
src                 └───┘    └───┘
typ                 └───┘    └───┘
doc                 └───┘    └───┘
628  begin
st   └─────
629    induction x with xl xr xL xR IHxl IHxr generalizing y,
id               
src    └────────┘ └────────────────────────────────────────┘
typ    └────────┘└────────────────────────────────────────┘
doc    └────────┘ └────────────────────────────────────────┘
txt    └────────┘ └────────────────────────────────────────┘
par    └────────┘ └────────────────────────────────────────┘
pid              └────────────────────────┘└─────────────┘
st   ──────────────────────────────────────────────────────┘└─
630    induction y with yl yr yL yR IHyl IHyr,
id               
src    └────────┘ └─────────────────────────┘
typ    └────────┘└─────────────────────────┘
doc    └────────┘ └─────────────────────────┘
txt    └────────┘ └─────────────────────────┘
par    └────────┘ └─────────────────────────┘
pid              └────────────────────────┘
st   ───────────────────────────────────────┘└─
631    have y := mk yl yr yL yR,
id               └┘ └┘ └┘ └┘ └┘
src    └────────┘└┘      
typ    └────────┘└┘└┘└┘└┘└┘
doc    └────────┘        
txt    └────────┘        
par    └────────┘        
pid    └────┘└─┘        
st   ─────────────────────────┘└─
632    refine ⟨xl ⊕ yl, xr ⊕ yr, sum.rec _ _, sum.rec _ _⟩,
id             └┘  └┘  └┘   └┘               └─────┘
src    └─────┘     └┘     └┘       └────┘└─────┘└───┘
typ    └─────┘ └┘└┘└┘└┘ └┘└┘       └────┘└─────┘└───┘
doc    └─────┘      └┘     └┘       └────┘       └───┘
txt    └─────┘      └┘     └┘       └────┘       └───┘
par    └─────┘      └┘     └┘       └────┘       └───┘
pid                └┘     └┘       └────┘       └───┘
st   ────────────────────────────────────────────────────┘└─
633    { exact λ i, IHxl i y },
id                  └──┘   
src      └────┘ └──┘      
typ      └────┘ └──┘└──┘ 
doc      └────┘ └──┘      
txt      └────┘ └──┘      
par      └────┘ └──┘      
pid            └──┘      
st   ───┘└──────────────────┘└┘
634    { exact λ i, IHyl i },
id                  └──┘
src      └────┘ └──┘     
typ      └────┘ └──┘└──┘ 
doc      └────┘ └──┘     
txt      └────┘ └──┘     
par      └────┘ └──┘     
pid            └──┘     
st   ───┘└────────────────┘└┘
635    { exact λ i, IHxr i y },
id                  └──┘   
src      └────┘ └──┘      
typ      └────┘ └──┘└──┘ 
doc      └────┘ └──┘      
txt      └────┘ └──┘      
par      └────┘ └──┘      
pid            └──┘      
st   ───┘└──────────────────┘└┘
636    { exact λ i, IHyr i }
id                  └──┘
src      └────┘ └──┘     
typ      └────┘ └──┘└──┘ 
doc      └────┘ └──┘     
txt      └────┘ └──┘     
par      └────┘ └──┘     
pid            └──┘     
st   ─────────────────────┘└─
637  end
st   ──┘
638  
639  instance : has_add pgame := ⟨add⟩
id              └─────┘ └───┘     └─┘
src             └─────┘ └───┘     └─┘
typ             └─────┘ └───┘     └─┘
doc                     └───┘     └─┘
640  
641  /-- `x + 0` has exactly the same moves as `x`. -/
642  def add_zero_relabelling : Π (x : pgame.{u}), relabelling (x + 0) x
id                                    └───┘       └─────────┘       
src                                    └───┘       └─────────┘    
typ                                   └───┘       └─────────┘       
doc                                    └───┘       └─────────┘
643  | (mk xl xr xL xR) :=
id      └┘
src     └┘
typ     └┘
644  begin
st   └─────
645    refine ⟨equiv.sum_pempty xl, equiv.sum_pempty xr, _, _⟩,
id                              └┘  └──────────────┘ └┘
src    └─────┘                   └┘└──────────────┘  └─────┘
typ    └─────┘                 └┘└┘└──────────────┘└┘└─────┘
doc    └─────┘                   └┘                  └─────┘
txt    └─────┘                   └┘                  └─────┘
par    └─────┘                   └┘                  └─────┘
pid                             └┘                  └─────┘
st   ────────────────────────────────────────────────────────┘└─
646    { rintro (⟨i⟩|⟨⟨⟩⟩),
src      └───────────────┘
typ      └───────────────┘
doc      └───────────────┘
txt      └───────────────┘
par      └───────────────┘
pid            └─────────┘
st   ───┘└───────────────┘└─
647      apply add_zero_relabelling, },
src      └────┘
typ      └────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ─────────────────────────────┘└──┘
648    { rintro j,
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid            └┘
st   ───────────┘└─
649      apply add_zero_relabelling, }
src      └────┘
typ      └────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ─────────────────────────────┘└───
650  end
st   ──┘
651  
652  /-- `x + 0` is equivalent to `x`. -/
653  lemma add_zero_equiv (x : pgame.{u}) : x + 0 ≈ x :=
id                             └───┘             
src                            └───┘             
typ                            └───┘             
doc                            └───┘              
654  equiv_of_relabelling (add_zero_relabelling x)
id   └──────────────────┘  └──────────────────┘ 
src  └──────────────────┘  └──────────────────┘
typ  └──────────────────┘  └──────────────────┘ 
doc  └──────────────────┘  └──────────────────┘
655  
656  /-- `0 + x` has exactly the same moves as `x`. -/
657  def zero_add_relabelling : Π (x : pgame.{u}), relabelling (0 + x) x
id                                    └───┘       └─────────┘       
src                                    └───┘       └─────────┘    
typ                                   └───┘       └─────────┘       
doc                                    └───┘       └─────────┘
658  | (mk xl xr xL xR) :=
id      └┘
src     └┘
typ     └┘
659  begin
st   └─────
660    refine ⟨equiv.pempty_sum xl, equiv.pempty_sum xr, _, _⟩,
id                              └┘  └──────────────┘ └┘
src    └─────┘                   └┘└──────────────┘  └─────┘
typ    └─────┘                 └┘└┘└──────────────┘└┘└─────┘
doc    └─────┘                   └┘                  └─────┘
txt    └─────┘                   └┘                  └─────┘
par    └─────┘                   └┘                  └─────┘
pid                             └┘                  └─────┘
st   ────────────────────────────────────────────────────────┘└─
661    { rintro (⟨⟨⟩⟩|⟨i⟩),
src      └───────────────┘
typ      └───────────────┘
doc      └───────────────┘
txt      └───────────────┘
par      └───────────────┘
pid            └─────────┘
st   ───┘└───────────────┘└─
662      apply zero_add_relabelling, },
src      └────┘
typ      └────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ─────────────────────────────┘└──┘
663    { rintro j,
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid            └┘
st   ───────────┘└─
664      apply zero_add_relabelling, }
src      └────┘
typ      └────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ─────────────────────────────┘└───
665  end
st   ──┘
666  
667  /-- `0 + x` is equivalent to `x`. -/
668  lemma zero_add_equiv (x : pgame.{u}) : 0 + x ≈ x :=
id                             └───┘             
src                            └───┘             
typ                            └───┘             
doc                            └───┘              
669  equiv_of_relabelling (zero_add_relabelling x)
id   └──────────────────┘  └──────────────────┘ 
src  └──────────────────┘  └──────────────────┘
typ  └──────────────────┘  └──────────────────┘ 
doc  └──────────────────┘  └──────────────────┘
670  
671  /-- An explicit equivalence between the moves for Left in `x + y` and the type-theory sum
672      of the moves for Left in `x` and in `y`. -/
673  def left_moves_add (x y : pgame) : (x + y).left_moves ≃ x.left_moves ⊕ y.left_moves :=
id                             └───┘        └────────┘   └─────────┘  └─────────┘
src                            └───┘          └────────┘    └─────────┘   └─────────┘
typ                            └───┘        └────────┘   └─────────┘  └─────────┘
doc                            └───┘           └────────┘    └─────────┘    └─────────┘
674  by { cases x, cases y, refl, }
id                      
src       └────┘   └────┘   └──┘
typ       └────┘  └────┘  └──┘
doc       └────┘   └────┘   └──┘
txt       └────┘   └────┘   └──┘
par       └────┘   └────┘   └──┘
pid                    
st     └────────┘└───────┘└────┘└──┘
675  
676  /-- An explicit equivalence between the moves for Right in `x + y` and the type-theory sum
677      of the moves for Right in `x` and in `y`. -/
678  def right_moves_add (x y : pgame) : (x + y).right_moves ≃ x.right_moves ⊕ y.right_moves :=
id                              └───┘        └─────────┘   └──────────┘  └──────────┘
src                             └───┘          └─────────┘    └──────────┘   └──────────┘
typ                             └───┘        └─────────┘   └──────────┘  └──────────┘
doc                             └───┘           └─────────┘    └──────────┘    └──────────┘
679  by { cases x, cases y, refl, }
id                      
src       └────┘   └────┘   └──┘
typ       └────┘  └────┘  └──┘
doc       └────┘   └────┘   └──┘
txt       └────┘   └────┘   └──┘
par       └────┘   └────┘   └──┘
pid                    
st     └────────┘└───────┘└────┘└──┘
680  
681  @[simp] lemma mk_add_move_left_inl {xl xr yl yr} {xL xR yL yR} {i} :
doc    └──┘
682    (mk xl xr xL xR + mk yl yr yL yR).move_left (sum.inl i) = (mk xl xr xL xR).move_left i + (mk yl yr yL yR) :=
id      └┘ └┘ └┘ └┘ └┘  └┘ └┘ └┘ └┘ └┘ └───────┘   └─────┘     └┘ └┘ └┘ └┘ └┘ └───────┘     └┘ └┘ └┘ └┘ └┘
src     └┘              └┘             └───────┘   └─────┘      └┘             └───────┘      └┘
typ     └┘ └┘ └┘ └┘ └┘  └┘ └┘ └┘ └┘ └┘ └───────┘   └─────┘     └┘ └┘ └┘ └┘ └┘ └───────┘     └┘ └┘ └┘ └┘ └┘
doc                                     └───────┘                                └───────┘
683  rfl
id   └─┘
src  └─┘
typ  └─┘
684  @[simp] lemma add_move_left_inl {x y : pgame} {i} :
id                                          └───┘
src                                         └───┘
typ                                         └───┘
doc    └──┘                                 └───┘
685    (x + y).move_left ((@left_moves_add x y).symm (sum.inl i)) = x.move_left i + y :=
id         └───────┘     └────────────┘   └──┘   └─────┘     └────────┘   
src          └───────┘     └────────────┘     └──┘   └─────┘       └────────┘   
typ        └───────┘     └────────────┘   └──┘   └─────┘     └────────┘   
doc           └───────┘     └────────────┘                           └────────┘
686  by { cases x, cases y, refl, }
id                      
src       └────┘   └────┘   └──┘
typ       └────┘  └────┘  └──┘
doc       └────┘   └────┘   └──┘
txt       └────┘   └────┘   └──┘
par       └────┘   └────┘   └──┘
pid                    
st     └────────┘└───────┘└────┘└──┘
687  
688  @[simp] lemma mk_add_move_right_inl {xl xr yl yr} {xL xR yL yR} {i} :
doc    └──┘
689    (mk xl xr xL xR + mk yl yr yL yR).move_right (sum.inl i) = (mk xl xr xL xR).move_right i + (mk yl yr yL yR) :=
id      └┘ └┘ └┘ └┘ └┘  └┘ └┘ └┘ └┘ └┘ └────────┘   └─────┘     └┘ └┘ └┘ └┘ └┘ └────────┘     └┘ └┘ └┘ └┘ └┘
src     └┘              └┘             └────────┘   └─────┘      └┘             └────────┘      └┘
typ     └┘ └┘ └┘ └┘ └┘  └┘ └┘ └┘ └┘ └┘ └────────┘   └─────┘     └┘ └┘ └┘ └┘ └┘ └────────┘     └┘ └┘ └┘ └┘ └┘
doc                                     └────────┘                                └────────┘
690  rfl
id   └─┘
src  └─┘
typ  └─┘
691  @[simp] lemma add_move_right_inl {x y : pgame} {i} :
id                                           └───┘
src                                          └───┘
typ                                          └───┘
doc    └──┘                                  └───┘
692    (x + y).move_right ((@right_moves_add x y).symm (sum.inl i)) = x.move_right i + y :=
id         └────────┘     └─────────────┘   └──┘   └─────┘     └─────────┘   
src          └────────┘     └─────────────┘     └──┘   └─────┘       └─────────┘   
typ        └────────┘     └─────────────┘   └──┘   └─────┘     └─────────┘   
doc           └────────┘     └─────────────┘                           └─────────┘
693  by { cases x, cases y, refl, }
id                      
src       └────┘   └────┘   └──┘
typ       └────┘  └────┘  └──┘
doc       └────┘   └────┘   └──┘
txt       └────┘   └────┘   └──┘
par       └────┘   └────┘   └──┘
pid                    
st     └────────┘└───────┘└────┘└──┘
694  
695  @[simp] lemma mk_add_move_left_inr {xl xr yl yr} {xL xR yL yR} {i} :
doc    └──┘
696    (mk xl xr xL xR + mk yl yr yL yR).move_left (sum.inr i) = (mk xl xr xL xR) + (mk yl yr yL yR).move_left i :=
id      └┘ └┘ └┘ └┘ └┘  └┘ └┘ └┘ └┘ └┘ └───────┘   └─────┘     └┘ └┘ └┘ └┘ └┘    └┘ └┘ └┘ └┘ └┘ └───────┘  
src     └┘              └┘             └───────┘   └─────┘      └┘                └┘             └───────┘
typ     └┘ └┘ └┘ └┘ └┘  └┘ └┘ └┘ └┘ └┘ └───────┘   └─────┘     └┘ └┘ └┘ └┘ └┘    └┘ └┘ └┘ └┘ └┘ └───────┘  
doc                                     └───────┘                                                   └───────┘
697  rfl
id   └─┘
src  └─┘
typ  └─┘
698  @[simp] lemma add_move_left_inr {x y : pgame} {i : y.left_moves} :
id                                          └───┘       └─────────┘
src                                         └───┘        └─────────┘
typ                                         └───┘       └─────────┘
doc    └──┘                                 └───┘        └─────────┘
699    (x + y).move_left ((@left_moves_add x y).symm (sum.inr i)) = x + y.move_left i :=
id         └───────┘     └────────────┘   └──┘   └─────┘       └────────┘ 
src          └───────┘     └────────────┘     └──┘   └─────┘          └────────┘
typ        └───────┘     └────────────┘   └──┘   └─────┘       └────────┘ 
doc           └───────┘     └────────────┘                               └────────┘
700  by { cases x, cases y, refl, }
id                      
src       └────┘   └────┘   └──┘
typ       └────┘  └────┘  └──┘
doc       └────┘   └────┘   └──┘
txt       └────┘   └────┘   └──┘
par       └────┘   └────┘   └──┘
pid                    
st     └────────┘└───────┘└────┘└──┘
701  
702  @[simp] lemma mk_add_move_right_inr {xl xr yl yr} {xL xR yL yR} {i} :
doc    └──┘
703    (mk xl xr xL xR + mk yl yr yL yR).move_right (sum.inr i) = (mk xl xr xL xR) + (mk yl yr yL yR).move_right i :=
id      └┘ └┘ └┘ └┘ └┘  └┘ └┘ └┘ └┘ └┘ └────────┘   └─────┘     └┘ └┘ └┘ └┘ └┘    └┘ └┘ └┘ └┘ └┘ └────────┘  
src     └┘              └┘             └────────┘   └─────┘      └┘                └┘             └────────┘
typ     └┘ └┘ └┘ └┘ └┘  └┘ └┘ └┘ └┘ └┘ └────────┘   └─────┘     └┘ └┘ └┘ └┘ └┘    └┘ └┘ └┘ └┘ └┘ └────────┘  
doc                                     └────────┘                                                   └────────┘
704  rfl
id   └─┘
src  └─┘
typ  └─┘
705  @[simp] lemma add_move_right_inr {x y : pgame} {i} :
id                                           └───┘
src                                          └───┘
typ                                          └───┘
doc    └──┘                                  └───┘
706    (x + y).move_right ((@right_moves_add x y).symm (sum.inr i)) = x + y.move_right i :=
id         └────────┘     └─────────────┘   └──┘   └─────┘       └─────────┘ 
src          └────────┘     └─────────────┘     └──┘   └─────┘          └─────────┘
typ        └────────┘     └─────────────┘   └──┘   └─────┘       └─────────┘ 
doc           └────────┘     └─────────────┘                               └─────────┘
707  by { cases x, cases y, refl, }
id                      
src       └────┘   └────┘   └──┘
typ       └────┘  └────┘  └──┘
doc       └────┘   └────┘   └──┘
txt       └────┘   └────┘   └──┘
par       └────┘   └────┘   └──┘
pid                    
st     └────────┘└───────┘└────┘└──┘
708  
709  instance : has_sub pgame := ⟨λ x y, x + -y⟩
id              └─────┘ └───┘            
src             └─────┘ └───┘               
typ             └─────┘ └───┘            
doc                     └───┘
710  
711  /-- `-(x+y)` has exactly the same moves as `-x + -y`. -/
712  def neg_add_relabelling : Π (x y : pgame), relabelling (-(x + y)) (-x + -y)
id                                     └───┘   └─────────┘           
src                                     └───┘   └─────────┘              
typ                                    └───┘   └─────────┘           
doc                                     └───┘   └─────────┘
713  | (mk xl xr xL xR) (mk yl yr yL yR) :=
id         └┘ └┘ └┘ └┘   └┘ └┘ └┘ └┘ └┘
src                      └┘
typ        └┘ └┘ └┘ └┘   └┘ └┘ └┘ └┘ └┘
714  ⟨equiv.refl _, equiv.refl _,
id    └────────┘    └────────┘
src   └────────┘    └────────┘
typ   └────────┘    └────────┘
715   λ j, sum.cases_on j
id        └──────────┘ 
src        └──────────┘
typ       └──────────┘ 
716     (λ j, neg_add_relabelling (xR j) (mk yl yr yL yR))
id           └─────────────────┘        └┘
src                                       └┘
typ          └─────────────────┘        └┘
717     (λ j, neg_add_relabelling (mk xl xr xL xR) (yR j)),
id           └─────────────────┘  └┘                  
src                                └┘
typ          └─────────────────┘  └┘                  
718   λ i, sum.cases_on i
id        └──────────┘ 
src        └──────────┘
typ       └──────────┘ 
719     (λ i, neg_add_relabelling (xL i) (mk yl yr yL yR))
id           └─────────────────┘        └┘
src                                       └┘
typ          └─────────────────┘        └┘
720     (λ i, neg_add_relabelling (mk xl xr xL xR) (yL i))⟩
id           └─────────────────┘  └┘                  
src                                └┘
typ          └─────────────────┘  └┘                  
721  using_well_founded { dec_tac := pgame_wf_tac }
id                                   └──────────┘
src                                  └──────────┘
typ                                  └──────────┘
doc                                  └──────────┘
722  
723  theorem neg_add_le {x y : pgame} : -(x + y) ≤ -x + -y :=
id                             └───┘            
src                            └───┘               
typ                            └───┘            
doc                            └───┘
724  le_of_relabelling (neg_add_relabelling x y)
id   └───────────────┘  └─────────────────┘  
src  └───────────────┘  └─────────────────┘
typ  └───────────────┘  └─────────────────┘  
doc                     └─────────────────┘
725  
726  /-- `x+y` has exactly the same moves as `y+x`. -/
727  def add_comm_relabelling : Π (x y : pgame.{u}), relabelling (x + y) (y + x)
id                                      └───┘       └─────────┘         
src                                      └───┘       └─────────┘           
typ                                     └───┘       └─────────┘         
doc                                      └───┘       └─────────┘
728  | (mk xl xr xL xR) (mk yl yr yL yR) :=
id                       └┘
src                      └┘
typ                      └┘
729  begin
st   └─────
730    refine ⟨equiv.sum_comm _ _, equiv.sum_comm _ _, _, _⟩,
id                                 └────────────┘
src    └─────┘               └────┘└────────────┘└─────────┘
typ    └─────┘               └────┘└────────────┘└─────────┘
doc    └─────┘               └────┘              └─────────┘
txt    └─────┘               └────┘              └─────────┘
par    └─────┘               └────┘              └─────────┘
pid                         └────┘              └─────────┘
st   ──────────────────────────────────────────────────────┘└─
731    { rintros (_|_); { dsimp [left_moves_add], apply add_comm_relabelling, } },
id                               └────────────┘
src      └───────────┘    └─────┘└────────────┘  └────┘
typ      └───────────┘    └─────┘└────────────┘  └────┘
doc      └───────────┘    └─────┘└────────────┘  └────┘
txt      └───────────┘    └─────┘                └────┘
par      └───────────┘    └─────┘                └────┘
pid             └────┘                              
st   ───┘└─────────────┘└──────────────────────┘└──────────────────────────┘└────┘
732    { rintros (_|_); { dsimp [right_moves_add], apply add_comm_relabelling, } },
id                               └─────────────┘
src      └───────────┘    └─────┘└─────────────┘  └────┘
typ      └───────────┘    └─────┘└─────────────┘  └────┘
doc      └───────────┘    └─────┘└─────────────┘  └────┘
txt      └───────────┘    └─────┘                 └────┘
par      └───────────┘    └─────┘                 └────┘
pid             └────┘                               
st   ──────────────────┘└───────────────────────┘└──────────────────────────┘└──────
733  end
st   ──┘
734  using_well_founded { dec_tac := pgame_wf_tac }
id                                   └──────────┘
src                                  └──────────┘
typ                                  └──────────┘
doc                                  └──────────┘
735  
736  theorem add_comm_le {x y : pgame} : x + y ≤ y + x :=
id                              └───┘          
src                             └───┘            
typ                             └───┘          
doc                             └───┘
737  le_of_relabelling (add_comm_relabelling x y)
id   └───────────────┘  └──────────────────┘  
src  └───────────────┘  └──────────────────┘
typ  └───────────────┘  └──────────────────┘  
doc                     └──────────────────┘
738  
739  theorem add_comm_equiv {x y : pgame} : x + y ≈ y + x :=
id                                 └───┘          
src                                └───┘            
typ                                └───┘          
doc                                └───┘          
740  equiv_of_relabelling (add_comm_relabelling x y)
id   └──────────────────┘  └──────────────────┘  
src  └──────────────────┘  └──────────────────┘
typ  └──────────────────┘  └──────────────────┘  
doc  └──────────────────┘  └──────────────────┘
741  
742  /-- `(x + y) + z` has exactly the same moves as `x + (y + z)`. -/
743  def add_assoc_relabelling : Π (x y z : pgame.{u}), relabelling ((x + y) + z) (x + (y + z))
id                                         └───┘       └─────────┘                
src                                         └───┘       └─────────┘                    
typ                                        └───┘       └─────────┘                
doc                                         └───┘       └─────────┘
744  | (mk xl xr xL xR) (mk yl yr yL yR) (mk zl zr zL zR) :=
id                                        └┘
src                                       └┘
typ                                       └┘
745  begin
st   └─────
746    refine ⟨equiv.sum_assoc _ _ _, equiv.sum_assoc _ _ _, _, _⟩,
id                                    └─────────────┘
src    └─────┘                └──────┘└─────────────┘└───────────┘
typ    └─────┘                └──────┘└─────────────┘└───────────┘
doc    └─────┘                └──────┘               └───────────┘
txt    └─────┘                └──────┘               └───────────┘
par    └─────┘                └──────┘               └───────────┘
pid                          └──────┘               └───────────┘
st   ────────────────────────────────────────────────────────────┘└─
747    { rintro (⟨i|i⟩|i),
src      └──────────────┘
typ      └──────────────┘
doc      └──────────────┘
txt      └──────────────┘
par      └──────────────┘
pid            └────────┘
st   ───┘└──────────────┘└─
748      { apply add_assoc_relabelling, },
src        └────┘
typ        └────┘
doc        └────┘
txt        └────┘
par        └────┘
pid             
st   ─────┘└─────────────────────────┘└──┘
749      { change relabelling
id                └─────────┘
src        └─────┘└─────────┘
typ        └─────┘└─────────┘
doc        └─────┘└─────────┘
txt        └─────┘           
par        └─────┘           
pid                         
st   ─────┘└──────────────────
750          (mk xl xr xL xR + yL i + mk zl zr zL zR) (mk xl xr xL xR + (yL i + mk zl zr zL zR)),
id                                                       └┘ └┘ └┘ └┘    └┘    └┘ └┘ └┘ └┘ └┘
src  ───────┘                         └┘                 └┘        └┘
typ  ───────┘                         └┘   └┘└┘└┘└┘  └┘ └┘└┘└┘└┘└┘└┘
doc  ───────┘                          └┘                           └┘
txt  ───────┘                          └┘                           └┘
par  ───────┘                          └┘                           └┘
pid  ───────┘                          └┘                           └┘
st   ──────────────────────────────────────────────────────────────────────────────────────────┘└─
751        apply add_assoc_relabelling, },
src        └────┘
typ        └────┘
doc        └────┘
txt        └────┘
par        └────┘
pid             
st   ────────────────────────────────┘└──┘
752      { change relabelling
id                └─────────┘
src        └─────┘└─────────┘
typ        └─────┘└─────────┘
doc        └─────┘└─────────┘
txt        └─────┘           
par        └─────┘           
pid                         
st   ─────────────────────────
753          (mk xl xr xL xR + mk yl yr yL yR + zL i) (mk xl xr xL xR + (mk yl yr yL yR + zL i)),
id                                                        └┘ └┘ └┘ └┘    └┘ └┘ └┘ └┘ └┘   └┘ 
src  ───────┘                          └┘             └┘            └┘
typ  ───────┘                          └┘   └┘└┘└┘└┘  └┘└┘└┘└┘└┘ └┘└┘
doc  ───────┘                          └┘                           └┘
txt  ───────┘                          └┘                           └┘
par  ───────┘                          └┘                           └┘
pid  ───────┘                          └┘                           └┘
st   ──────────────────────────────────────────────────────────────────────────────────────────┘└─
754        apply add_assoc_relabelling, } },
src        └────┘
typ        └────┘
doc        └────┘
txt        └────┘
par        └────┘
pid             
st   ────────────────────────────────┘└────┘
755    { rintro (j|⟨j|j⟩),
src      └──────────────┘
typ      └──────────────┘
doc      └──────────────┘
txt      └──────────────┘
par      └──────────────┘
pid            └────────┘
st   ───────────────────┘└─
756      { apply add_assoc_relabelling, },
src        └────┘
typ        └────┘
doc        └────┘
txt        └────┘
par        └────┘
pid             
st   ─────┘└─────────────────────────┘└──┘
757      { change relabelling
id                └─────────┘
src        └─────┘└─────────┘
typ        └─────┘└─────────┘
doc        └─────┘└─────────┘
txt        └─────┘           
par        └─────┘           
pid                         
st   ─────┘└──────────────────
758          (mk xl xr xL xR + yR j + mk zl zr zL zR) (mk xl xr xL xR + (yR j + mk zl zr zL zR)),
id                                                        └┘ └┘ └┘ └┘    └┘    └┘ └┘ └┘ └┘ └┘
src  ───────┘                          └┘                 └┘        └┘
typ  ───────┘                          └┘   └┘└┘└┘└┘  └┘ └┘└┘└┘└┘└┘└┘
doc  ───────┘                          └┘                           └┘
txt  ───────┘                          └┘                           └┘
par  ───────┘                          └┘                           └┘
pid  ───────┘                          └┘                           └┘
st   ──────────────────────────────────────────────────────────────────────────────────────────┘└─
759        apply add_assoc_relabelling, },
src        └────┘
typ        └────┘
doc        └────┘
txt        └────┘
par        └────┘
pid             
st   ────────────────────────────────┘└──┘
760      { change relabelling
id                └─────────┘
src        └─────┘└─────────┘
typ        └─────┘└─────────┘
doc        └─────┘└─────────┘
txt        └─────┘           
par        └─────┘           
pid                         
st   ─────────────────────────
761          (mk xl xr xL xR + mk yl yr yL yR + zR j) (mk xl xr xL xR + (mk yl yr yL yR + zR j)),
id                                                        └┘ └┘ └┘ └┘    └┘ └┘ └┘ └┘ └┘   └┘ 
src  ───────┘                          └┘             └┘            └┘
typ  ───────┘                          └┘   └┘└┘└┘└┘  └┘└┘└┘└┘└┘ └┘└┘
doc  ───────┘                          └┘                           └┘
txt  ───────┘                          └┘                           └┘
par  ───────┘                          └┘                           └┘
pid  ───────┘                          └┘                           └┘
st   ──────────────────────────────────────────────────────────────────────────────────────────┘└─
762        apply add_assoc_relabelling, } },
src        └────┘
typ        └────┘
doc        └────┘
txt        └────┘
par        └────┘
pid             
st   ────────────────────────────────┘└──────
763  end
st   ──┘
764  using_well_founded { dec_tac := pgame_wf_tac }
id                                   └──────────┘
src                                  └──────────┘
typ                                  └──────────┘
doc                                  └──────────┘
765  
766  theorem add_assoc_equiv {x y z : pgame} : (x + y) + z ≈ x + (y + z) :=
id                                    └───┘                 
src                                   └───┘                     
typ                                   └───┘                 
doc                                   └───┘                
767  equiv_of_relabelling (add_assoc_relabelling x y z)
id   └──────────────────┘  └───────────────────┘   
src  └──────────────────┘  └───────────────────┘
typ  └──────────────────┘  └───────────────────┘   
doc  └──────────────────┘  └───────────────────┘
768  
769  theorem add_le_add_right : Π {x y z : pgame} (h : x ≤ y), x + z ≤ y + z
id                                        └───┘                  
src                                       └───┘                      
typ                                       └───┘                  
doc                                        └───┘
770  | (mk xl xr xL xR) (mk yl yr yL yR) (mk zl zr zL zR) :=
id                                        └┘
src                                       └┘
typ                                       └┘
771  begin
st   └─────
772    intros h,
src    └──────┘
typ    └──────┘
doc    └──────┘
txt    └──────┘
par    └──────┘
pid          └┘
st   ─────────┘└─
773    rw le_def,
id        └────┘
src    └─┘└────┘
typ    └─┘└────┘
doc    └─┘└────┘
txt    └─┘
par    └─┘
pid      
st   ──────────┘└─
774    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
775    { -- if Left plays first
st   ───┘└──────────────────────
776      intros i,
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid            └┘
st   ───────────┘└─
777      change xl ⊕ zl at i,
id              └┘  └┘
src      └─────┘    └───┘
typ      └─────┘└┘└┘└───┘
doc      └─────┘     └───┘
txt      └─────┘     └───┘
par      └─────┘     └───┘
pid                 └──┘
st   ──────────────────────┘└─
778      cases i,
id             
src      └────┘
typ      └────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ──────────┘└─
779      { -- either they play in x
st   ─────┘└────────────────────────
780        rw le_def at h,
id            └────┘
src        └─┘└────┘└───┘
typ        └─┘└────┘└───┘
doc        └─┘└────┘└───┘
txt        └─┘      └───┘
par        └─┘      └───┘
pid                └───┘
st   ───────────────────┘└─
781        cases h,
id               
src        └────┘
typ        └────┘
doc        └────┘
txt        └────┘
par        └────┘
pid             
st   ────────────┘└─
782        have t := h_left i,
id                   └────┘ 
src        └────────┘      
typ        └────────┘└────┘
doc        └────────┘      
txt        └────────┘      
par        └────────┘      
pid        └────┘└─┘      
st   ───────────────────────┘└─
783        rcases t with ⟨i', ih⟩ | ⟨j, jh⟩,
id                
src        └─────┘ └──────────────────────┘
typ        └─────┘└──────────────────────┘
doc        └─────┘ └──────────────────────┘
txt        └─────┘ └──────────────────────┘
par        └─────┘ └──────────────────────┘
pid               └──────────────────────┘
st   ─────────────────────────────────────┘└─
784        { left,
src          └──┘
typ          └──┘
doc          └──┘
txt          └──┘
par          └──┘
st   ───────┘└──┘└─
785          refine ⟨(left_moves_add _ _).inv_fun (sum.inl i'), _⟩,
id                    └────────────┘               └─────┘ └┘
src          └─────┘  └────────────┘└────────────┘ └─────┘  └───┘
typ          └─────┘  └────────────┘└────────────┘ └─────┘└┘└───┘
doc          └─────┘  └────────────┘└────────────┘          └───┘
txt          └─────┘                └────────────┘          └───┘
par          └─────┘                └────────────┘          └───┘
pid                                └────────────┘          └───┘
st   ────────────────────────────────────────────────────────────┘└─
786          exact add_le_add_right ih, },
id                 └──────────────┘ └┘
src          └────┘└──────────────┘
typ          └────┘└──────────────┘└┘
doc          └────┘                
txt          └────┘                
par          └────┘                
pid                               
st   ────────────────────────────────┘└──┘
787        { right,
src          └───┘
typ          └───┘
doc          └───┘
txt          └───┘
par          └───┘
st   ────────────┘└─
788          refine ⟨(right_moves_add _ _).inv_fun (sum.inl j), _⟩,
id                    └─────────────┘               └─────┘ 
src          └─────┘  └─────────────┘└────────────┘ └─────┘ └───┘
typ          └─────┘  └─────────────┘└────────────┘ └─────┘└───┘
doc          └─────┘  └─────────────┘└────────────┘         └───┘
txt          └─────┘                 └────────────┘         └───┘
par          └─────┘                 └────────────┘         └───┘
pid                                 └────────────┘         └───┘
st   ────────────────────────────────────────────────────────────┘└─
789          convert add_le_add_right jh,
id                   └──────────────┘ └┘
src          └──────┘└──────────────┘
typ          └──────┘└──────────────┘└┘
doc          └──────┘                
txt          └──────┘                
par          └──────┘                
pid                                 
st   ──────────────────────────────────┘└─
790          apply add_move_right_inl },
id                 └────────────────┘
src          └────┘└────────────────┘
typ          └────┘└────────────────┘
doc          └────┘                  
txt          └────┘                  
par          └────┘                  
pid                                 
st   ────────────────────────────────┘└──
791        },
st   ───────┘
792      { -- or play in z
st   ──────────────────────
793        left,
src        └──┘
typ        └──┘
doc        └──┘
txt        └──┘
par        └──┘
st   ─────────┘└─
794        refine ⟨(left_moves_add _ _).inv_fun (sum.inr i), _⟩,
id                  └────────────┘               └─────┘ 
src        └─────┘  └────────────┘└────────────┘ └─────┘ └───┘
typ        └─────┘  └────────────┘└────────────┘ └─────┘└───┘
doc        └─────┘  └────────────┘└────────────┘         └───┘
txt        └─────┘                └────────────┘         └───┘
par        └─────┘                └────────────┘         └───┘
pid                              └────────────┘         └───┘
st   ─────────────────────────────────────────────────────────┘└─
795        exact add_le_add_right h, }, },
id               └──────────────┘ 
src        └────┘└──────────────┘
typ        └────┘└──────────────┘
doc        └────┘                
txt        └────┘                
par        └────┘                
pid                             
st   ─────────────────────────────┘└─────┘
796    { -- if Right plays first
st   ────────────────────────────
797      intros j,
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid            └┘
st   ───────────┘└─
798      change yr ⊕ zr at j,
id              └┘   └┘
src      └─────┘     └───┘
typ      └─────┘└┘ └┘└───┘
doc      └─────┘     └───┘
txt      └─────┘     └───┘
par      └─────┘     └───┘
pid                 └──┘
st   ──────────────────────┘└─
799      cases j,
id             
src      └────┘
typ      └────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ──────────┘└─
800      { -- either they play in y
st   ─────┘└────────────────────────
801        rw le_def at h,
id            └────┘
src        └─┘└────┘└───┘
typ        └─┘└────┘└───┘
doc        └─┘└────┘└───┘
txt        └─┘      └───┘
par        └─┘      └───┘
pid                └───┘
st   ───────────────────┘└─
802        cases h,
id               
src        └────┘
typ        └────┘
doc        └────┘
txt        └────┘
par        └────┘
pid             
st   ────────────┘└─
803        have t := h_right j,
id                   └─────┘ 
src        └────────┘       
typ        └────────┘└─────┘
doc        └────────┘       
txt        └────────┘       
par        └────────┘       
pid        └────┘└─┘       
st   ────────────────────────┘└─
804        rcases t with ⟨i, ih⟩ | ⟨j', jh⟩,
id                
src        └─────┘ └──────────────────────┘
typ        └─────┘└──────────────────────┘
doc        └─────┘ └──────────────────────┘
txt        └─────┘ └──────────────────────┘
par        └─────┘ └──────────────────────┘
pid               └──────────────────────┘
st   ─────────────────────────────────────┘└─
805        { left,
src          └──┘
typ          └──┘
doc          └──┘
txt          └──┘
par          └──┘
st   ───────┘└──┘└─
806          refine ⟨(left_moves_add _ _).inv_fun (sum.inl i), _⟩,
id                    └────────────┘               └─────┘ 
src          └─────┘  └────────────┘└────────────┘ └─────┘ └───┘
typ          └─────┘  └────────────┘└────────────┘ └─────┘└───┘
doc          └─────┘  └────────────┘└────────────┘         └───┘
txt          └─────┘                └────────────┘         └───┘
par          └─────┘                └────────────┘         └───┘
pid                                └────────────┘         └───┘
st   ───────────────────────────────────────────────────────────┘└─
807          convert add_le_add_right ih,
id                   └──────────────┘ └┘
src          └──────┘└──────────────┘
typ          └──────┘└──────────────┘└┘
doc          └──────┘                
txt          └──────┘                
par          └──────┘                
pid                                 
st   ──────────────────────────────────┘└─
808          apply add_move_left_inl },
id                 └───────────────┘
src          └────┘└───────────────┘
typ          └────┘└───────────────┘
doc          └────┘                 
txt          └────┘                 
par          └────┘                 
pid                                
st   ───────────────────────────────┘└┘
809        { right,
src          └───┘
typ          └───┘
doc          └───┘
txt          └───┘
par          └───┘
st   ────────────┘└─
810          refine ⟨(right_moves_add _ _).inv_fun (sum.inl j'), _⟩,
id                    └─────────────┘               └─────┘ └┘
src          └─────┘  └─────────────┘└────────────┘ └─────┘  └───┘
typ          └─────┘  └─────────────┘└────────────┘ └─────┘└┘└───┘
doc          └─────┘  └─────────────┘└────────────┘          └───┘
txt          └─────┘                 └────────────┘          └───┘
par          └─────┘                 └────────────┘          └───┘
pid                                 └────────────┘          └───┘
st   ─────────────────────────────────────────────────────────────┘└─
811          exact add_le_add_right jh } },
id                 └──────────────┘ └┘
src          └────┘└──────────────┘  
typ          └────┘└──────────────┘└┘
doc          └────┘                  
txt          └────┘                  
par          └────┘                  
pid                                 
st   ─────────────────────────────────┘└──┘
812      { -- or play in z
st   ──────────────────────
813        right,
src        └───┘
typ        └───┘
doc        └───┘
txt        └───┘
par        └───┘
st   ──────────┘└─
814        refine ⟨(right_moves_add _ _).inv_fun (sum.inr j), _⟩,
id                  └─────────────┘               └─────┘ 
src        └─────┘  └─────────────┘└────────────┘ └─────┘ └───┘
typ        └─────┘  └─────────────┘└────────────┘ └─────┘└───┘
doc        └─────┘  └─────────────┘└────────────┘         └───┘
txt        └─────┘                 └────────────┘         └───┘
par        └─────┘                 └────────────┘         └───┘
pid                               └────────────┘         └───┘
st   ──────────────────────────────────────────────────────────┘└─
815        exact add_le_add_right h } }
id               └──────────────┘ 
src        └────┘└──────────────┘ 
typ        └────┘└──────────────┘
doc        └────┘                 
txt        └────┘                 
par        └────┘                 
pid                              
st   ──────────────────────────────┘└───
816  end
st   ──┘
817  using_well_founded { dec_tac := pgame_wf_tac }
id                                   └──────────┘
src                                  └──────────┘
typ                                  └──────────┘
doc                                  └──────────┘
818  
819  theorem add_le_add_left {x y z : pgame} (h : y ≤ z) : x + y ≤ x + z :=
id                                    └───┘                   
src                                   └───┘                       
typ                                   └───┘                   
doc                                   └───┘
820  calc x + y ≤ y + x : add_comm_le
id                  └─────────┘
src                     └─────────┘
typ                 └─────────┘
821       ... ≤ z + x : add_le_add_right h
id                   └──────────────┘ 
src                    └──────────────┘
typ                  └──────────────┘ 
822       ... ≤ x + z : add_comm_le
id                   └─────────┘
src                    └─────────┘
typ                  └─────────┘
823  
824  theorem add_congr {w x y z : pgame} (h₁ : w ≈ x) (h₂ : y ≈ z) : w + y ≈ x + z :=
id                                └───┘                              
src                               └───┘                                    
typ                               └───┘                              
doc                               └───┘                                  
825  ⟨calc w + y ≤ w + z : add_le_add_left h₂.1
id                   └─────────────┘ └┘
src                      └─────────────┘   
typ                  └─────────────┘ └┘
826          ... ≤ x + z : add_le_add_right h₁.1,
id                      └──────────────┘ └┘
src                       └──────────────┘   
typ                     └──────────────┘ └┘
827   calc x + z ≤ x + y : add_le_add_left h₂.2
id                   └─────────────┘ └┘
src                      └─────────────┘   
typ                  └─────────────┘ └┘
828          ... ≤ w + y : add_le_add_right h₁.2⟩
id                      └──────────────┘ └┘
src                       └──────────────┘   
typ                     └──────────────┘ └┘
829  
830  theorem add_left_neg_le_zero : Π {x : pgame}, (-x) + x ≤ 0
id                                        └───┘        
src                                        └───┘          
typ                                       └───┘        
doc                                        └───┘
831  | ⟨xl, xr, xL, xR⟩ :=
832  begin
st   └─────
833    rw [le_def],
id         └────┘
src    └──┘└────┘
typ    └──┘└────┘
doc    └──┘└────┘
txt    └──┘      
par    └──┘      
pid      └┘      
st   ───────────┘└──
834    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
835    { intro i,
src      └─────┘
typ      └─────┘
doc      └─────┘
txt      └─────┘
par      └─────┘
pid           └┘
st   ───┘└─────┘└─
836      change xr ⊕ xl at i,
id              └┘  └┘
src      └─────┘    └───┘
typ      └─────┘└┘└┘└───┘
doc      └─────┘     └───┘
txt      └─────┘     └───┘
par      └─────┘     └───┘
pid                 └──┘
st   ──────────────────────┘└─
837      cases i,
id             
src      └────┘
typ      └────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ──────────┘└─
838      { -- If Left played in -x, Right responds with the same move in x.
st   ─────┘└────────────────────────────────────────────────────────────────
839        right,
src        └───┘
typ        └───┘
doc        └───┘
txt        └───┘
par        └───┘
st   ──────────┘└─
840        refine ⟨(right_moves_add _ _).inv_fun (sum.inr i), _⟩,
id                  └─────────────┘               └─────┘ 
src        └─────┘  └─────────────┘└────────────┘ └─────┘ └───┘
typ        └─────┘  └─────────────┘└────────────┘ └─────┘└───┘
doc        └─────┘  └─────────────┘└────────────┘         └───┘
txt        └─────┘                 └────────────┘         └───┘
par        └─────┘                 └────────────┘         └───┘
pid                               └────────────┘         └───┘
st   ──────────────────────────────────────────────────────────┘└─
841        convert @add_left_neg_le_zero (xR i),
id                  └──────────────────┘  └┘ 
src        └──────┘                         
typ        └──────┘ └──────────────────┘ └┘
doc        └──────┘                         
txt        └──────┘                         
par        └──────┘                         
pid                                        
st   ─────────────────────────────────────────┘└─
842        exact add_move_right_inr },
id               └────────────────┘
src        └────┘└────────────────┘
typ        └────┘└────────────────┘
doc        └────┘                  
txt        └────┘                  
par        └────┘                  
pid                               
st   ──────────────────────────────┘└┘
843      { -- If Left in x, Right responds with the same move in -x.
st   ────────────────────────────────────────────────────────────────
844        right,
src        └───┘
typ        └───┘
doc        └───┘
txt        └───┘
par        └───┘
st   ──────────┘└─
845        dsimp,
src        └───┘
typ        └───┘
doc        └───┘
txt        └───┘
par        └───┘
st   ──────────┘└─
846        refine ⟨(right_moves_add _ _).inv_fun (sum.inl i), _⟩,
id                  └─────────────┘               └─────┘ 
src        └─────┘  └─────────────┘└────────────┘ └─────┘ └───┘
typ        └─────┘  └─────────────┘└────────────┘ └─────┘└───┘
doc        └─────┘  └─────────────┘└────────────┘         └───┘
txt        └─────┘                 └────────────┘         └───┘
par        └─────┘                 └────────────┘         └───┘
pid                               └────────────┘         └───┘
st   ──────────────────────────────────────────────────────────┘└─
847        convert @add_left_neg_le_zero (xL i),
id                  └──────────────────┘  └┘ 
src        └──────┘                         
typ        └──────┘ └──────────────────┘ └┘
doc        └──────┘                         
txt        └──────┘                         
par        └──────┘                         
pid                                        
st   ─────────────────────────────────────────┘└─
848        exact add_move_right_inl }, },
id               └────────────────┘
src        └────┘└────────────────┘
typ        └────┘└────────────────┘
doc        └────┘                  
txt        └────┘                  
par        └────┘                  
pid                               
st   ──────────────────────────────┘└───┘
849    { rintro ⟨⟩, }
src      └───────┘
typ      └───────┘
doc      └───────┘
txt      └───────┘
par      └───────┘
pid            └─┘
st   ────────────┘└───
850  end
st   ──┘
851  using_well_founded { dec_tac := pgame_wf_tac }
id                                   └──────────┘
src                                  └──────────┘
typ                                  └──────────┘
doc                                  └──────────┘
852  
853  theorem zero_le_add_left_neg : Π {x : pgame}, 0 ≤ (-x) + x :=
id                                         └───┘          
src                                        └───┘          
typ                                        └───┘          
doc                                        └───┘
854  begin
st   └─────
855    intro x,
src    └─────┘
typ    └─────┘
doc    └─────┘
txt    └─────┘
par    └─────┘
pid         └┘
st   ────────┘└─
856    rw [le_iff_neg_ge, neg_zero],
id         └───────────┘  └──────┘
src    └──┘└───────────┘└┘└──────┘
typ    └──┘└───────────┘└┘└──────┘
doc    └──┘             └┘        
txt    └──┘             └┘        
par    └──┘             └┘        
pid      └┘             └┘        
st   ──────────────────┘└────────┘└──
857    exact le_trans neg_add_le add_left_neg_le_zero
id           └──────┘ └────────┘ └──────────────────┘
src    └────┘└──────┘└────────┘└──────────────────┘
typ    └────┘└──────┘└────────┘└──────────────────┘
doc    └────┘                                      
txt    └────┘                                      
par    └────┘                                      
pid                                               
st   ────────────────────────────────────────────────┘
858  end
st   └─┘
859  
860  theorem add_left_neg_equiv {x : pgame} : (-x) + x ≈ 0 :=
id                                   └───┘         
src                                  └───┘           
typ                                  └───┘         
doc                                  └───┘             
861  ⟨add_left_neg_le_zero, zero_le_add_left_neg⟩
id    └──────────────────┘  └──────────────────┘
src   └──────────────────┘  └──────────────────┘
typ   └──────────────────┘  └──────────────────┘
862  
863  theorem add_right_neg_le_zero {x : pgame} : x + (-x) ≤ 0 :=
id                                      └───┘         
src                                     └───┘           
typ                                     └───┘         
doc                                     └───┘
864  calc x + (-x) ≤ (-x) + x : add_comm_le
id                      └─────────┘
src                         └─────────┘
typ                     └─────────┘
865       ... ≤ 0 : add_left_neg_le_zero
id                  └──────────────────┘
src                 └──────────────────┘
typ                 └──────────────────┘
866  
867  theorem zero_le_add_right_neg {x : pgame} : 0 ≤ x + (-x) :=
id                                      └───┘          
src                                     └───┘           
typ                                     └───┘          
doc                                     └───┘
868  calc 0 ≤ (-x) + x : zero_le_add_left_neg
id                   └──────────────────┘
src                    └──────────────────┘
typ                  └──────────────────┘
869       ... ≤ x + (-x) : add_comm_le
id                     └─────────┘
src                      └─────────┘
typ                    └─────────┘
870  
871  theorem add_lt_add_right {x y z : pgame} (h : x < y) : x + z < y + z :=
id                                     └───┘                   
src                                    └───┘                       
typ                                    └───┘                   
doc                                    └───┘
872  suffices y + z ≤ x + z → y ≤ x, by { rw ←not_le at ⊢ h, exact mt this h },
id                                  └────┘               └┘ └──┘ 
src                                   └──┘└────┘└─────┘  └────┘└┘     
typ                             └──┘└────┘└─────┘  └────┘└┘└──┘
doc                                       └──┘      └─────┘  └────┘       
txt                                       └──┘      └─────┘  └────┘       
par                                       └──┘      └─────┘  └────┘       
pid                                         └┘      └─────┘              
st                                     └──────────────────┘└────────────────┘└┘
873  assume w,
id          
typ         
874  calc y ≤ y + 0            : le_of_relabelling (add_zero_relabelling _).symm
id                            └───────────────┘  └──────────────────┘   └──┘
src                             └───────────────┘  └──────────────────┘   └──┘
typ                           └───────────────┘  └──────────────────┘   └──┘
doc                                                 └──────────────────┘   └──┘
875       ... ≤ y + (z + -z)   : add_le_add_left zero_le_add_right_neg
id                         └─────────────┘ └───────────────────┘
src                           └─────────────┘ └───────────────────┘
typ                        └─────────────┘ └───────────────────┘
876       ... ≤ (y + z) + (-z) : le_of_relabelling (add_assoc_relabelling _ _ _).symm
id                         └───────────────┘  └───────────────────┘       └──┘
src                           └───────────────┘  └───────────────────┘       └──┘
typ                        └───────────────┘  └───────────────────┘       └──┘
doc                                                 └───────────────────┘       └──┘
877       ... ≤ (x + z) + (-z) : add_le_add_right w
id                         └──────────────┘ 
src                           └──────────────┘
typ                        └──────────────┘ 
878       ... ≤ x + (z + -z)   : le_of_relabelling (add_assoc_relabelling _ _ _)
id                         └───────────────┘  └───────────────────┘
src                           └───────────────┘  └───────────────────┘
typ                        └───────────────┘  └───────────────────┘
doc                                                 └───────────────────┘
879       ... ≤ x + 0          : add_le_add_left add_right_neg_le_zero
id                             └─────────────┘ └───────────────────┘
src                             └─────────────┘ └───────────────────┘
typ                            └─────────────┘ └───────────────────┘
880       ... ≤ x              : le_of_relabelling (add_zero_relabelling _)
id                              └───────────────┘  └──────────────────┘
src                              └───────────────┘  └──────────────────┘
typ                             └───────────────┘  └──────────────────┘
doc                                                 └──────────────────┘
881  
882  theorem add_lt_add_left {x y z : pgame} (h : y < z) : x + y < x + z :=
id                                    └───┘                   
src                                   └───┘                       
typ                                   └───┘                   
doc                                   └───┘
883  calc x + y ≤ y + x : add_comm_le
id                  └─────────┘
src                     └─────────┘
typ                 └─────────┘
884       ... < z + x   : add_lt_add_right h
id                     └──────────────┘ 
src                      └──────────────┘
typ                    └──────────────┘ 
885       ... ≤ x + z   : add_comm_le
id                     └─────────┘
src                      └─────────┘
typ                    └─────────┘
886  
887  theorem le_iff_sub_nonneg {x y : pgame} : x ≤ y ↔ 0 ≤ y - x :=
id                                    └───┘             
src                                   └───┘               
typ                                   └───┘             
doc                                   └───┘
888  ⟨λ h, le_trans zero_le_add_right_neg (add_le_add_right h),
id        └──────┘ └───────────────────┘  └──────────────┘ 
src        └──────┘ └───────────────────┘  └──────────────┘
typ       └──────┘ └───────────────────┘  └──────────────┘ 
889   λ h,
id      
typ     
890    calc x ≤ 0 + x : le_of_relabelling (zero_add_relabelling x).symm
id                   └───────────────┘  └──────────────────┘  └──┘
src                    └───────────────┘  └──────────────────┘   └──┘
typ                  └───────────────┘  └──────────────────┘  └──┘
doc                                        └──────────────────┘   └──┘
891       ... ≤ (y - x) + x : add_le_add_right h
id                       └──────────────┘ 
src                         └──────────────┘
typ                      └──────────────┘ 
892       ... ≤ y + (-x + x) : le_of_relabelling (add_assoc_relabelling _ _ _)
id                       └───────────────┘  └───────────────────┘
src                         └───────────────┘  └───────────────────┘
typ                      └───────────────┘  └───────────────────┘
doc                                               └───────────────────┘
893       ... ≤ y + 0 : add_le_add_left (add_left_neg_le_zero)
id                    └─────────────┘  └──────────────────┘
src                    └─────────────┘  └──────────────────┘
typ                   └─────────────┘  └──────────────────┘
894       ... ≤ y : le_of_relabelling (add_zero_relabelling y)⟩
id                 └───────────────┘  └──────────────────┘ 
src                 └───────────────┘  └──────────────────┘
typ                └───────────────┘  └──────────────────┘ 
doc                                    └──────────────────┘
895  theorem lt_iff_sub_pos {x y : pgame} : x < y ↔ 0 < y - x :=
id                                 └───┘             
src                                └───┘               
typ                                └───┘             
doc                                └───┘
896  ⟨λ h, lt_of_le_of_lt zero_le_add_right_neg (add_lt_add_right h),
id        └────────────┘ └───────────────────┘  └──────────────┘ 
src        └────────────┘ └───────────────────┘  └──────────────┘
typ       └────────────┘ └───────────────────┘  └──────────────┘ 
897   λ h,
id      
typ     
898    calc x ≤ 0 + x : le_of_relabelling (zero_add_relabelling x).symm
id                   └───────────────┘  └──────────────────┘  └──┘
src                    └───────────────┘  └──────────────────┘   └──┘
typ                  └───────────────┘  └──────────────────┘  └──┘
doc                                        └──────────────────┘   └──┘
899       ... < (y - x) + x : add_lt_add_right h
id                       └──────────────┘ 
src                         └──────────────┘
typ                      └──────────────┘ 
900       ... ≤ y + (-x + x) : le_of_relabelling (add_assoc_relabelling _ _ _)
id                       └───────────────┘  └───────────────────┘
src                         └───────────────┘  └───────────────────┘
typ                      └───────────────┘  └───────────────────┘
doc                                               └───────────────────┘
901       ... ≤ y + 0 : add_le_add_left (add_left_neg_le_zero)
id                    └─────────────┘  └──────────────────┘
src                    └─────────────┘  └──────────────────┘
typ                   └─────────────┘  └──────────────────┘
902       ... ≤ y : le_of_relabelling (add_zero_relabelling y)⟩
id                 └───────────────┘  └──────────────────┘ 
src                 └───────────────┘  └──────────────────┘
typ                └───────────────┘  └──────────────────┘ 
doc                                    └──────────────────┘
903  
904  /-- The pre-game `star`, which is fuzzy/confused with zero. -/
905  def star : pgame := pgame.of_lists [0] [0]
id              └───┘    └────────────┘    
src             └───┘    └────────────┘    
typ             └───┘    └────────────┘    
doc             └───┘    └────────────┘
906  
907  theorem star_lt_zero : star < 0 :=
id                          └──┘ 
src                         └──┘ 
typ                         └──┘ 
doc                         └──┘
908  or.inr ⟨⟨0, zero_lt_one⟩, (by split; rintros ⟨⟩)⟩
id   └────┘      └─────────┘
src  └────┘      └─────────┘       └───┘  └────────┘
typ  └────┘      └─────────┘       └───┘  └────────┘
doc                                └───┘  └────────┘
txt                                └───┘  └────────┘
par                                └───┘  └────────┘
pid                                              └─┘
st                                └────────────────┘
909  
910  theorem zero_lt_star : 0 < star :=
id                             └──┘
src                            └──┘
typ                            └──┘
doc                             └──┘
911  or.inl ⟨⟨0, zero_lt_one⟩, (by split; rintros ⟨⟩)⟩
id   └────┘      └─────────┘
src  └────┘      └─────────┘       └───┘  └────────┘
typ  └────┘      └─────────┘       └───┘  └────────┘
doc                                └───┘  └────────┘
txt                                └───┘  └────────┘
par                                └───┘  └────────┘
pid                                              └─┘
st                                └────────────────┘
912  
913  /-- The pre-game `ω`. (In fact all ordinals have game and surreal representatives.) -/
914  def omega : pgame := ⟨ulift ℕ, pempty, λ n, ↑n.1, pempty.elim⟩
id               └───┘     └───┘   └────┘         └─────────┘
src              └───┘     └───┘   └────┘           └─────────┘
typ              └───┘     └───┘   └────┘         └─────────┘
doc              └───┘     └───┘    └────┘
915  
916  end pgame